text: Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvrabcsf Structured version   Visualization version   GIF version
  
  Theorem cbvrabcsf 3601
   Description: A more general version of cbvrab 3229 with no distinct variable restrictions. (Contributed by Andrew Salmon, 13-Jul-2011.)
  Hypotheses
  Ref Expression
  cbvralcsf.1 𝑦𝐴
  cbvralcsf.2 𝑥𝐵
  cbvralcsf.3 𝑦𝜑
  cbvralcsf.4 𝑥𝜓
  cbvralcsf.5 (𝑥 = 𝑦𝐴 = 𝐵)
  cbvralcsf.6 (𝑥 = 𝑦 → (𝜑𝜓))
  Assertion
  Ref Expression
  cbvrabcsf {𝑥𝐴𝜑} = {𝑦𝐵𝜓}
  
  Proof of Theorem cbvrabcsf
  Dummy variables 𝑣 𝑧 are mutually distinct and distinct from all other variables.
  StepHypRef Expression
  1 nfv 1883 . . . 4 𝑧(𝑥𝐴𝜑)
  2 nfcsb1v 3582 . . . . . 6 𝑥𝑧 / 𝑥𝐴
  32nfcri 2787 . . . . 5 𝑥 𝑧𝑧 / 𝑥𝐴
  4 nfs1v 2465 . . . . 5 𝑥[𝑧 / 𝑥]𝜑
  53, 4nfan 1868 . . . 4 𝑥(𝑧𝑧 / 𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑)
  6 id 22 . . . . . 6 (𝑥 = 𝑧𝑥 = 𝑧)
  7 csbeq1a 3575 . . . . . 6 (𝑥 = 𝑧𝐴 = 𝑧 / 𝑥𝐴)
  86, 7eleq12d 2724 . . . . 5 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝑧 / 𝑥𝐴))
  9 sbequ12 2149 . . . . 5 (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
  108, 9anbi12d 747 . . . 4 (𝑥 = 𝑧 → ((𝑥𝐴𝜑) ↔ (𝑧𝑧 / 𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑)))
  111, 5, 10cbvab 2775 . . 3 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑧 ∣ (𝑧𝑧 / 𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑)}
  12 nfcv 2793 . . . . . . 7 𝑦𝑧
  13 cbvralcsf.1 . . . . . . 7 𝑦𝐴
  1412, 13nfcsb 3584 . . . . . 6 𝑦𝑧 / 𝑥𝐴
  1514nfcri 2787 . . . . 5 𝑦 𝑧𝑧 / 𝑥𝐴
  16 cbvralcsf.3 . . . . . 6 𝑦𝜑
  1716nfsb 2468 . . . . 5 𝑦[𝑧 / 𝑥]𝜑
  1815, 17nfan 1868 . . . 4 𝑦(𝑧𝑧 / 𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑)
  19 nfv 1883 . . . 4 𝑧(𝑦𝐵𝜓)
  20 id 22 . . . . . 6 (𝑧 = 𝑦𝑧 = 𝑦)
  21 csbeq1 3569 . . . . . . 7 (𝑧 = 𝑦𝑧 / 𝑥𝐴 = 𝑦 / 𝑥𝐴)
  22 df-csb 3567 . . . . . . . 8 𝑦 / 𝑥𝐴 = {𝑣[𝑦 / 𝑥]𝑣𝐴}
  23 cbvralcsf.2 . . . . . . . . . . . 12 𝑥𝐵
  2423nfcri 2787 . . . . . . . . . . 11 𝑥 𝑣𝐵
  25 cbvralcsf.5 . . . . . . . . . . . 12 (𝑥 = 𝑦𝐴 = 𝐵)
  2625eleq2d 2716 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑣𝐴𝑣𝐵))
  2724, 26sbie 2436 . . . . . . . . . 10 ([𝑦 / 𝑥]𝑣𝐴𝑣𝐵)
  28 sbsbc 3472 . . . . . . . . . 10 ([𝑦 / 𝑥]𝑣𝐴[𝑦 / 𝑥]𝑣𝐴)
  2927, 28bitr3i 266 . . . . . . . . 9 (𝑣𝐵[𝑦 / 𝑥]𝑣𝐴)
  3029abbi2i 2767 . . . . . . . 8 𝐵 = {𝑣[𝑦 / 𝑥]𝑣𝐴}
  3122, 30eqtr4i 2676 . . . . . . 7 𝑦 / 𝑥𝐴 = 𝐵
  3221, 31syl6eq 2701 . . . . . 6 (𝑧 = 𝑦𝑧 / 𝑥𝐴 = 𝐵)
  3320, 32eleq12d 2724 . . . . 5 (𝑧 = 𝑦 → (𝑧𝑧 / 𝑥𝐴𝑦𝐵))
  34 sbequ 2404 . . . . . 6 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
  35 cbvralcsf.4 . . . . . . 7 𝑥𝜓
  36 cbvralcsf.6 . . . . . . 7 (𝑥 = 𝑦 → (𝜑𝜓))
  3735, 36sbie 2436 . . . . . 6 ([𝑦 / 𝑥]𝜑𝜓)
  3834, 37syl6bb 276 . . . . 5 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑𝜓))
  3933, 38anbi12d 747 . . . 4 (𝑧 = 𝑦 → ((𝑧𝑧 / 𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑) ↔ (𝑦𝐵𝜓)))
  4018, 19, 39cbvab 2775 . . 3 {𝑧 ∣ (𝑧𝑧 / 𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑)} = {𝑦 ∣ (𝑦𝐵𝜓)}
  4111, 40eqtri 2673 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑦 ∣ (𝑦𝐵𝜓)}
  42 df-rab 2950 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
  43 df-rab 2950 . 2 {𝑦𝐵𝜓} = {𝑦 ∣ (𝑦𝐵𝜓)}
  4441, 42, 433eqtr4i 2683 1 {𝑥𝐴𝜑} = {𝑦𝐵𝜓}
   Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523  Ⅎwnf 1748  [wsb 1937   ∈ wcel 2030  {cab 2637  Ⅎwnfc 2780  {crab 2945  [wsbc 3468  ⦋csb 3566 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-sbc 3469  df-csb 3567 This theorem is referenced by:  cbvrabv2  39625  smfsup  41341  smfinflem  41344  smfinf  41345
   Copyright terms: Public domain W3C validator
explanation: The provided text is a formal proof in the Metamath Proof Explorer, a project that aims to develop a comprehensive database of mathematical proofs. The text describes a theorem (cbvrabcsf) and its proof, which involves variable substitution and class abstraction. The theorem is about a more general version of variable substitution in restricted class abstractions without distinct variable restrictions.
  
  The text does not contain a math question or an answer to a question. It is a formal proof of a theorem.
distilabel_metadata.content: Evaluate the user given text extract and determine if it contains a math question and optionally and answer to this question.
  
  Output rules:
  
  1. Briefly describe the document and mention if it contains a question or a question and answer.
  2. Finalize the output with: Label: no-question,question,question-and-answer,multiple-question,multiple-question-and-answer
distilabel_metadata.role: system
distilabel_metadata.content: Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvrabcsf Structured version   Visualization version   GIF version
  
  Theorem cbvrabcsf 3601
   Description: A more general version of cbvrab 3229 with no distinct variable restrictions. (Contributed by Andrew Salmon, 13-Jul-2011.)
  Hypotheses
  Ref Expression
  cbvralcsf.1 𝑦𝐴
  cbvralcsf.2 𝑥𝐵
  cbvralcsf.3 𝑦𝜑
  cbvralcsf.4 𝑥𝜓
  cbvralcsf.5 (𝑥 = 𝑦𝐴 = 𝐵)
  cbvralcsf.6 (𝑥 = 𝑦 → (𝜑𝜓))
  Assertion
  Ref Expression
  cbvrabcsf {𝑥𝐴𝜑} = {𝑦𝐵𝜓}
  
  Proof of Theorem cbvrabcsf
  Dummy variables 𝑣 𝑧 are mutually distinct and distinct from all other variables.
  StepHypRef Expression
  1 nfv 1883 . . . 4 𝑧(𝑥𝐴𝜑)
  2 nfcsb1v 3582 . . . . . 6 𝑥𝑧 / 𝑥𝐴
  32nfcri 2787 . . . . 5 𝑥 𝑧𝑧 / 𝑥𝐴
  4 nfs1v 2465 . . . . 5 𝑥[𝑧 / 𝑥]𝜑
  53, 4nfan 1868 . . . 4 𝑥(𝑧𝑧 / 𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑)
  6 id 22 . . . . . 6 (𝑥 = 𝑧𝑥 = 𝑧)
  7 csbeq1a 3575 . . . . . 6 (𝑥 = 𝑧𝐴 = 𝑧 / 𝑥𝐴)
  86, 7eleq12d 2724 . . . . 5 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝑧 / 𝑥𝐴))
  9 sbequ12 2149 . . . . 5 (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
  108, 9anbi12d 747 . . . 4 (𝑥 = 𝑧 → ((𝑥𝐴𝜑) ↔ (𝑧𝑧 / 𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑)))
  111, 5, 10cbvab 2775 . . 3 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑧 ∣ (𝑧𝑧 / 𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑)}
  12 nfcv 2793 . . . . . . 7 𝑦𝑧
  13 cbvralcsf.1 . . . . . . 7 𝑦𝐴
  1412, 13nfcsb 3584 . . . . . 6 𝑦𝑧 / 𝑥𝐴
  1514nfcri 2787 . . . . 5 𝑦 𝑧𝑧 / 𝑥𝐴
  16 cbvralcsf.3 . . . . . 6 𝑦𝜑
  1716nfsb 2468 . . . . 5 𝑦[𝑧 / 𝑥]𝜑
  1815, 17nfan 1868 . . . 4 𝑦(𝑧𝑧 / 𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑)
  19 nfv 1883 . . . 4 𝑧(𝑦𝐵𝜓)
  20 id 22 . . . . . 6 (𝑧 = 𝑦𝑧 = 𝑦)
  21 csbeq1 3569 . . . . . . 7 (𝑧 = 𝑦𝑧 / 𝑥𝐴 = 𝑦 / 𝑥𝐴)
  22 df-csb 3567 . . . . . . . 8 𝑦 / 𝑥𝐴 = {𝑣[𝑦 / 𝑥]𝑣𝐴}
  23 cbvralcsf.2 . . . . . . . . . . . 12 𝑥𝐵
  2423nfcri 2787 . . . . . . . . . . 11 𝑥 𝑣𝐵
  25 cbvralcsf.5 . . . . . . . . . . . 12 (𝑥 = 𝑦𝐴 = 𝐵)
  2625eleq2d 2716 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑣𝐴𝑣𝐵))
  2724, 26sbie 2436 . . . . . . . . . 10 ([𝑦 / 𝑥]𝑣𝐴𝑣𝐵)
  28 sbsbc 3472 . . . . . . . . . 10 ([𝑦 / 𝑥]𝑣𝐴[𝑦 / 𝑥]𝑣𝐴)
  2927, 28bitr3i 266 . . . . . . . . 9 (𝑣𝐵[𝑦 / 𝑥]𝑣𝐴)
  3029abbi2i 2767 . . . . . . . 8 𝐵 = {𝑣[𝑦 / 𝑥]𝑣𝐴}
  3122, 30eqtr4i 2676 . . . . . . 7 𝑦 / 𝑥𝐴 = 𝐵
  3221, 31syl6eq 2701 . . . . . 6 (𝑧 = 𝑦𝑧 / 𝑥𝐴 = 𝐵)
  3320, 32eleq12d 2724 . . . . 5 (𝑧 = 𝑦 → (𝑧𝑧 / 𝑥𝐴𝑦𝐵))
  34 sbequ 2404 . . . . . 6 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
  35 cbvralcsf.4 . . . . . . 7 𝑥𝜓
  36 cbvralcsf.6 . . . . . . 7 (𝑥 = 𝑦 → (𝜑𝜓))
  3735, 36sbie 2436 . . . . . 6 ([𝑦 / 𝑥]𝜑𝜓)
  3834, 37syl6bb 276 . . . . 5 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑𝜓))
  3933, 38anbi12d 747 . . . 4 (𝑧 = 𝑦 → ((𝑧𝑧 / 𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑) ↔ (𝑦𝐵𝜓)))
  4018, 19, 39cbvab 2775 . . 3 {𝑧 ∣ (𝑧𝑧 / 𝑥𝐴 ∧ [𝑧 / 𝑥]𝜑)} = {𝑦 ∣ (𝑦𝐵𝜓)}
  4111, 40eqtri 2673 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑦 ∣ (𝑦𝐵𝜓)}
  42 df-rab 2950 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
  43 df-rab 2950 . 2 {𝑦𝐵𝜓} = {𝑦 ∣ (𝑦𝐵𝜓)}
  4441, 42, 433eqtr4i 2683 1 {𝑥𝐴𝜑} = {𝑦𝐵𝜓}
   Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523  Ⅎwnf 1748  [wsb 1937   ∈ wcel 2030  {cab 2637  Ⅎwnfc 2780  {crab 2945  [wsbc 3468  ⦋csb 3566 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-sbc 3469  df-csb 3567 This theorem is referenced by:  cbvrabv2  39625  smfsup  41341  smfinflem  41344  smfinf  41345
   Copyright terms: Public domain W3C validator
distilabel_metadata.role: user
distilabel_metadata.raw_output_q_a_detector_0: The provided text is a formal proof in the Metamath Proof Explorer, a project that aims to develop a comprehensive database of mathematical proofs. The text describes a theorem (cbvrabcsf) and its proof, which involves variable substitution and class abstraction. The theorem is about a more general version of variable substitution in restricted class abstractions without distinct variable restrictions.
  
  The text does not contain a math question or an answer to a question. It is a formal proof of a theorem.
  
  Label: no-question