Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvrab Structured version   Visualization version   GIF version

Theorem cbvrab 3229
 Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 9-Oct-2016.)
Hypotheses
Ref Expression
cbvrab.1 𝑥𝐴
cbvrab.2 𝑦𝐴
cbvrab.3 𝑦𝜑
cbvrab.4 𝑥𝜓
cbvrab.5 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvrab {𝑥𝐴𝜑} = {𝑦𝐴𝜓}

Proof of Theorem cbvrab
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 nfv 1883 . . . 4 𝑧(𝑥𝐴𝜑)
2 cbvrab.1 . . . . . 6 𝑥𝐴
32nfcri 2787 . . . . 5 𝑥 𝑧𝐴
4 nfs1v 2465 . . . . 5 𝑥[𝑧 / 𝑥]𝜑
53, 4nfan 1868 . . . 4 𝑥(𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)
6 eleq1 2718 . . . . 5 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
7 sbequ12 2149 . . . . 5 (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
86, 7anbi12d 747 . . . 4 (𝑥 = 𝑧 → ((𝑥𝐴𝜑) ↔ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)))
91, 5, 8cbvab 2775 . . 3 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑧 ∣ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)}
10 cbvrab.2 . . . . . 6 𝑦𝐴
1110nfcri 2787 . . . . 5 𝑦 𝑧𝐴
12 cbvrab.3 . . . . . 6 𝑦𝜑
1312nfsb 2468 . . . . 5 𝑦[𝑧 / 𝑥]𝜑
1411, 13nfan 1868 . . . 4 𝑦(𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)
15 nfv 1883 . . . 4 𝑧(𝑦𝐴𝜓)
16 eleq1 2718 . . . . 5 (𝑧 = 𝑦 → (𝑧𝐴𝑦𝐴))
17 sbequ 2404 . . . . . 6 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
18 cbvrab.4 . . . . . . 7 𝑥𝜓
19 cbvrab.5 . . . . . . 7 (𝑥 = 𝑦 → (𝜑𝜓))
2018, 19sbie 2436 . . . . . 6 ([𝑦 / 𝑥]𝜑𝜓)
2117, 20syl6bb 276 . . . . 5 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑𝜓))
2216, 21anbi12d 747 . . . 4 (𝑧 = 𝑦 → ((𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑) ↔ (𝑦𝐴𝜓)))
2314, 15, 22cbvab 2775 . . 3 {𝑧 ∣ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)} = {𝑦 ∣ (𝑦𝐴𝜓)}
249, 23eqtri 2673 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑦 ∣ (𝑦𝐴𝜓)}
25 df-rab 2950 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
26 df-rab 2950 . 2 {𝑦𝐴𝜓} = {𝑦 ∣ (𝑦𝐴𝜓)}
2724, 25, 263eqtr4i 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 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 This theorem is referenced by:  cbvrabv  3230  elrabsf  3507  tfis  7096  cantnflem1  8624  scottexs  8788  scott0s  8789  elmptrab  21678  bnj1534  31049  scottexf  34106  scott0f  34107  eq0rabdioph  37657  rexrabdioph  37675  rexfrabdioph  37676  elnn0rabdioph  37684  dvdsrabdioph  37691  binomcxplemdvsum  38871  fnlimcnv  40217  fnlimabslt  40229  stoweidlem34  40569  stoweidlem59  40594  pimltmnf2  41232  pimgtpnf2  41238  pimltpnf2  41244  issmff  41264  smfpimltxrmpt  41288  smfpreimagtf  41297  smflim  41306  smfpimgtxr  41309  smfpimgtxrmpt  41313  smflim2  41333  smflimsup  41355  smfliminf  41358
 Copyright terms: Public domain W3C validator