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

Theorem cbvrab 3347
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 2009 . . . 4 𝑧(𝑥𝐴𝜑)
2 cbvrab.1 . . . . . 6 𝑥𝐴
32nfcri 2901 . . . . 5 𝑥 𝑧𝐴
4 nfs1v 2287 . . . . 5 𝑥[𝑧 / 𝑥]𝜑
53, 4nfan 1998 . . . 4 𝑥(𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)
6 eleq1w 2827 . . . . 5 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
7 sbequ12 2278 . . . . 5 (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
86, 7anbi12d 624 . . . 4 (𝑥 = 𝑧 → ((𝑥𝐴𝜑) ↔ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)))
91, 5, 8cbvab 2889 . . 3 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑧 ∣ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)}
10 cbvrab.2 . . . . . 6 𝑦𝐴
1110nfcri 2901 . . . . 5 𝑦 𝑧𝐴
12 cbvrab.3 . . . . . 6 𝑦𝜑
1312nfsb 2534 . . . . 5 𝑦[𝑧 / 𝑥]𝜑
1411, 13nfan 1998 . . . 4 𝑦(𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)
15 nfv 2009 . . . 4 𝑧(𝑦𝐴𝜓)
16 eleq1w 2827 . . . . 5 (𝑧 = 𝑦 → (𝑧𝐴𝑦𝐴))
17 sbequ 2467 . . . . . 6 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
18 cbvrab.4 . . . . . . 7 𝑥𝜓
19 cbvrab.5 . . . . . . 7 (𝑥 = 𝑦 → (𝜑𝜓))
2018, 19sbie 2499 . . . . . 6 ([𝑦 / 𝑥]𝜑𝜓)
2117, 20syl6bb 278 . . . . 5 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑𝜓))
2216, 21anbi12d 624 . . . 4 (𝑧 = 𝑦 → ((𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑) ↔ (𝑦𝐴𝜓)))
2314, 15, 22cbvab 2889 . . 3 {𝑧 ∣ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)} = {𝑦 ∣ (𝑦𝐴𝜓)}
249, 23eqtri 2787 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑦 ∣ (𝑦𝐴𝜓)}
25 df-rab 3064 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
26 df-rab 3064 . 2 {𝑦𝐴𝜓} = {𝑦 ∣ (𝑦𝐴𝜓)}
2724, 25, 263eqtr4i 2797 1 {𝑥𝐴𝜑} = {𝑦𝐴𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wnf 1878  [wsb 2062  wcel 2155  {cab 2751  wnfc 2894  {crab 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-rab 3064
This theorem is referenced by:  cbvrabv  3348  elrabsf  3635  f1ossf1o  6586  tfis  7252  cantnflem1  8801  scottexs  8965  scott0s  8966  elmptrab  21910  bnj1534  31303  scottexf  34329  scott0f  34330  eq0rabdioph  37950  rexrabdioph  37968  rexfrabdioph  37969  elnn0rabdioph  37977  dvdsrabdioph  37984  binomcxplemdvsum  39160  fnlimcnv  40469  fnlimabslt  40481  stoweidlem34  40820  stoweidlem59  40845  pimltmnf2  41483  pimgtpnf2  41489  pimltpnf2  41495  issmff  41515  smfpimltxrmpt  41539  smfpreimagtf  41548  smflim  41557  smfpimgtxr  41560  smfpimgtxrmpt  41564  smflim2  41584  smflimsup  41606  smfliminf  41609
  Copyright terms: Public domain W3C validator