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

Theorem cbvrab 3411
 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 1873 . . . 4 𝑧(𝑥𝐴𝜑)
2 cbvrab.1 . . . . . 6 𝑥𝐴
32nfcri 2926 . . . . 5 𝑥 𝑧𝐴
4 nfs1v 2202 . . . . 5 𝑥[𝑧 / 𝑥]𝜑
53, 4nfan 1862 . . . 4 𝑥(𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)
6 eleq1w 2848 . . . . 5 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
7 sbequ12 2179 . . . . 5 (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
86, 7anbi12d 621 . . . 4 (𝑥 = 𝑧 → ((𝑥𝐴𝜑) ↔ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)))
91, 5, 8cbvab 2911 . . 3 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑧 ∣ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)}
10 cbvrab.2 . . . . . 6 𝑦𝐴
1110nfcri 2926 . . . . 5 𝑦 𝑧𝐴
12 cbvrab.3 . . . . . 6 𝑦𝜑
1312nfsb 2488 . . . . 5 𝑦[𝑧 / 𝑥]𝜑
1411, 13nfan 1862 . . . 4 𝑦(𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)
15 nfv 1873 . . . 4 𝑧(𝑦𝐴𝜓)
16 eleq1w 2848 . . . . 5 (𝑧 = 𝑦 → (𝑧𝐴𝑦𝐴))
17 sbequ 2035 . . . . . 6 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
18 cbvrab.4 . . . . . . 7 𝑥𝜓
19 cbvrab.5 . . . . . . 7 (𝑥 = 𝑦 → (𝜑𝜓))
2018, 19sbie 2468 . . . . . 6 ([𝑦 / 𝑥]𝜑𝜓)
2117, 20syl6bb 279 . . . . 5 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑𝜓))
2216, 21anbi12d 621 . . . 4 (𝑧 = 𝑦 → ((𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑) ↔ (𝑦𝐴𝜓)))
2314, 15, 22cbvab 2911 . . 3 {𝑧 ∣ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)} = {𝑦 ∣ (𝑦𝐴𝜓)}
249, 23eqtri 2802 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑦 ∣ (𝑦𝐴𝜓)}
25 df-rab 3097 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
26 df-rab 3097 . 2 {𝑦𝐴𝜓} = {𝑦 ∣ (𝑦𝐴𝜓)}
2724, 25, 263eqtr4i 2812 1 {𝑥𝐴𝜑} = {𝑦𝐴𝜓}
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1507  Ⅎwnf 1746  [wsb 2015   ∈ wcel 2050  {cab 2758  Ⅎwnfc 2916  {crab 3092 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-rab 3097 This theorem is referenced by:  cbvrabvOLD  3413  elrabsf  3720  f1ossf1o  6713  tfis  7385  cantnflem1  8946  scottexs  9110  scott0s  9111  elmptrab  22139  bnj1534  31778  scottexf  34896  scott0f  34897  eq0rabdioph  38775  rexrabdioph  38793  rexfrabdioph  38794  elnn0rabdioph  38802  dvdsrabdioph  38809  binomcxplemdvsum  40109  fnlimcnv  41385  fnlimabslt  41397  stoweidlem34  41756  stoweidlem59  41781  pimltmnf2  42416  pimgtpnf2  42422  pimltpnf2  42428  issmff  42448  smfpimltxrmpt  42472  smfpreimagtf  42481  smflim  42490  smfpimgtxr  42493  smfpimgtxrmpt  42497  smflim2  42517  smflimsup  42539  smfliminf  42542
 Copyright terms: Public domain W3C validator