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

Theorem cbvrab 3171
 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 1830 . . . 4 𝑧(𝑥𝐴𝜑)
2 cbvrab.1 . . . . . 6 𝑥𝐴
32nfcri 2745 . . . . 5 𝑥 𝑧𝐴
4 nfs1v 2425 . . . . 5 𝑥[𝑧 / 𝑥]𝜑
53, 4nfan 1816 . . . 4 𝑥(𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)
6 eleq1 2676 . . . . 5 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
7 sbequ12 2097 . . . . 5 (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
86, 7anbi12d 743 . . . 4 (𝑥 = 𝑧 → ((𝑥𝐴𝜑) ↔ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)))
91, 5, 8cbvab 2733 . . 3 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑧 ∣ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)}
10 cbvrab.2 . . . . . 6 𝑦𝐴
1110nfcri 2745 . . . . 5 𝑦 𝑧𝐴
12 cbvrab.3 . . . . . 6 𝑦𝜑
1312nfsb 2428 . . . . 5 𝑦[𝑧 / 𝑥]𝜑
1411, 13nfan 1816 . . . 4 𝑦(𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)
15 nfv 1830 . . . 4 𝑧(𝑦𝐴𝜓)
16 eleq1 2676 . . . . 5 (𝑧 = 𝑦 → (𝑧𝐴𝑦𝐴))
17 sbequ 2364 . . . . . 6 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
18 cbvrab.4 . . . . . . 7 𝑥𝜓
19 cbvrab.5 . . . . . . 7 (𝑥 = 𝑦 → (𝜑𝜓))
2018, 19sbie 2396 . . . . . 6 ([𝑦 / 𝑥]𝜑𝜓)
2117, 20syl6bb 275 . . . . 5 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑𝜓))
2216, 21anbi12d 743 . . . 4 (𝑧 = 𝑦 → ((𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑) ↔ (𝑦𝐴𝜓)))
2314, 15, 22cbvab 2733 . . 3 {𝑧 ∣ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)} = {𝑦 ∣ (𝑦𝐴𝜓)}
249, 23eqtri 2632 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑦 ∣ (𝑦𝐴𝜓)}
25 df-rab 2905 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
26 df-rab 2905 . 2 {𝑦𝐴𝜓} = {𝑦 ∣ (𝑦𝐴𝜓)}
2724, 25, 263eqtr4i 2642 1 {𝑥𝐴𝜑} = {𝑦𝐴𝜓}
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  Ⅎwnf 1699  [wsb 1867   ∈ wcel 1977  {cab 2596  Ⅎwnfc 2738  {crab 2900 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905 This theorem is referenced by:  cbvrabv  3172  elrabsf  3441  tfis  6946  cantnflem1  8469  scottexs  8633  scott0s  8634  elmptrab  21440  bnj1534  30177  scottexf  33146  scott0f  33147  eq0rabdioph  36358  rexrabdioph  36376  rexfrabdioph  36377  elnn0rabdioph  36385  dvdsrabdioph  36392  binomcxplemdvsum  37576  fnlimcnv  38734  fnlimabslt  38746  stoweidlem34  38927  stoweidlem59  38952  pimltmnf2  39588  pimgtpnf2  39594  pimltpnf2  39600  issmff  39620  smfpimltxrmpt  39645  smfpreimagtf  39654  smflim  39663  smfpimgtxr  39666  smfpimgtxrmpt  39670
 Copyright terms: Public domain W3C validator