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

Theorem cbvrabw 3468
Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. Version of cbvrab 3474 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Andrew Salmon, 11-Jul-2011.) Avoid ax-13 2372. (Revised by Gino Giotto, 10-Jan-2024.)
Hypotheses
Ref Expression
cbvrabw.1 𝑥𝐴
cbvrabw.2 𝑦𝐴
cbvrabw.3 𝑦𝜑
cbvrabw.4 𝑥𝜓
cbvrabw.5 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvrabw {𝑥𝐴𝜑} = {𝑦𝐴𝜓}
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)   𝐴(𝑥,𝑦)

Proof of Theorem cbvrabw
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 nfv 1918 . . . 4 𝑧(𝑥𝐴𝜑)
2 cbvrabw.1 . . . . . 6 𝑥𝐴
32nfcri 2891 . . . . 5 𝑥 𝑧𝐴
4 nfs1v 2154 . . . . 5 𝑥[𝑧 / 𝑥]𝜑
53, 4nfan 1903 . . . 4 𝑥(𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)
6 eleq1w 2817 . . . . 5 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
7 sbequ12 2244 . . . . 5 (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
86, 7anbi12d 632 . . . 4 (𝑥 = 𝑧 → ((𝑥𝐴𝜑) ↔ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)))
91, 5, 8cbvabw 2807 . . 3 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑧 ∣ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)}
10 cbvrabw.2 . . . . . 6 𝑦𝐴
1110nfcri 2891 . . . . 5 𝑦 𝑧𝐴
12 cbvrabw.3 . . . . . 6 𝑦𝜑
1312nfsbv 2324 . . . . 5 𝑦[𝑧 / 𝑥]𝜑
1411, 13nfan 1903 . . . 4 𝑦(𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)
15 nfv 1918 . . . 4 𝑧(𝑦𝐴𝜓)
16 eleq1w 2817 . . . . 5 (𝑧 = 𝑦 → (𝑧𝐴𝑦𝐴))
17 sbequ 2087 . . . . . 6 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
18 cbvrabw.4 . . . . . . 7 𝑥𝜓
19 cbvrabw.5 . . . . . . 7 (𝑥 = 𝑦 → (𝜑𝜓))
2018, 19sbiev 2309 . . . . . 6 ([𝑦 / 𝑥]𝜑𝜓)
2117, 20bitrdi 287 . . . . 5 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑𝜓))
2216, 21anbi12d 632 . . . 4 (𝑧 = 𝑦 → ((𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑) ↔ (𝑦𝐴𝜓)))
2314, 15, 22cbvabw 2807 . . 3 {𝑧 ∣ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)} = {𝑦 ∣ (𝑦𝐴𝜓)}
249, 23eqtri 2761 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑦 ∣ (𝑦𝐴𝜓)}
25 df-rab 3434 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
26 df-rab 3434 . 2 {𝑦𝐴𝜓} = {𝑦 ∣ (𝑦𝐴𝜓)}
2724, 25, 263eqtr4i 2771 1 {𝑥𝐴𝜑} = {𝑦𝐴𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wnf 1786  [wsb 2068  wcel 2107  {cab 2710  wnfc 2884  {crab 3433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-rab 3434
This theorem is referenced by:  elrabsf  3826  f1ossf1o  7126  tfis  7844  cantnflem1  9684  scottexs  9882  scott0s  9883  elmptrab  23331  bnj1534  33864  scottexf  37036  scott0f  37037  eq0rabdioph  41514  rexrabdioph  41532  rexfrabdioph  41533  elnn0rabdioph  41541  dvdsrabdioph  41548  binomcxplemdvsum  43114  fnlimcnv  44383  fnlimabslt  44395  stoweidlem34  44750  stoweidlem59  44775  pimltmnf2f  45413  pimgtpnf2f  45421  pimltpnf2f  45428  issmff  45450  smfpimltxrmptf  45474  smfpreimagtf  45484  smflim  45493  smfpimgtxr  45496  smfpimgtxrmptf  45500  smflim2  45522  smflimsup  45544  smfliminf  45547
  Copyright terms: Public domain W3C validator