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

Theorem cbvrab 3348
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 1995 . . . 4 𝑧(𝑥𝐴𝜑)
2 cbvrab.1 . . . . . 6 𝑥𝐴
32nfcri 2907 . . . . 5 𝑥 𝑧𝐴
4 nfs1v 2274 . . . . 5 𝑥[𝑧 / 𝑥]𝜑
53, 4nfan 1980 . . . 4 𝑥(𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)
6 eleq1w 2833 . . . . 5 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
7 sbequ12 2267 . . . . 5 (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
86, 7anbi12d 616 . . . 4 (𝑥 = 𝑧 → ((𝑥𝐴𝜑) ↔ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)))
91, 5, 8cbvab 2895 . . 3 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑧 ∣ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)}
10 cbvrab.2 . . . . . 6 𝑦𝐴
1110nfcri 2907 . . . . 5 𝑦 𝑧𝐴
12 cbvrab.3 . . . . . 6 𝑦𝜑
1312nfsb 2590 . . . . 5 𝑦[𝑧 / 𝑥]𝜑
1411, 13nfan 1980 . . . 4 𝑦(𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)
15 nfv 1995 . . . 4 𝑧(𝑦𝐴𝜓)
16 eleq1w 2833 . . . . 5 (𝑧 = 𝑦 → (𝑧𝐴𝑦𝐴))
17 sbequ 2523 . . . . . 6 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
18 cbvrab.4 . . . . . . 7 𝑥𝜓
19 cbvrab.5 . . . . . . 7 (𝑥 = 𝑦 → (𝜑𝜓))
2018, 19sbie 2555 . . . . . 6 ([𝑦 / 𝑥]𝜑𝜓)
2117, 20syl6bb 276 . . . . 5 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑𝜓))
2216, 21anbi12d 616 . . . 4 (𝑧 = 𝑦 → ((𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑) ↔ (𝑦𝐴𝜓)))
2314, 15, 22cbvab 2895 . . 3 {𝑧 ∣ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)} = {𝑦 ∣ (𝑦𝐴𝜓)}
249, 23eqtri 2793 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑦 ∣ (𝑦𝐴𝜓)}
25 df-rab 3070 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
26 df-rab 3070 . 2 {𝑦𝐴𝜓} = {𝑦 ∣ (𝑦𝐴𝜓)}
2724, 25, 263eqtr4i 2803 1 {𝑥𝐴𝜑} = {𝑦𝐴𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wnf 1856  [wsb 2049  wcel 2145  {cab 2757  wnfc 2900  {crab 3065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070
This theorem is referenced by:  cbvrabv  3349  elrabsf  3626  f1ossf1o  6538  tfis  7201  cantnflem1  8750  scottexs  8914  scott0s  8915  elmptrab  21851  dlwwlknondlwlknonf1oOLD  27556  bnj1534  31261  scottexf  34308  scott0f  34309  eq0rabdioph  37866  rexrabdioph  37884  rexfrabdioph  37885  elnn0rabdioph  37893  dvdsrabdioph  37900  binomcxplemdvsum  39080  fnlimcnv  40417  fnlimabslt  40429  stoweidlem34  40768  stoweidlem59  40793  pimltmnf2  41431  pimgtpnf2  41437  pimltpnf2  41443  issmff  41463  smfpimltxrmpt  41487  smfpreimagtf  41496  smflim  41505  smfpimgtxr  41508  smfpimgtxrmpt  41512  smflim2  41532  smflimsup  41554  smfliminf  41557
  Copyright terms: Public domain W3C validator