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

Theorem cbvrabw 3465
Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. Version of cbvrab 3471 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by Andrew Salmon, 11-Jul-2011.) Avoid ax-13 2369. (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 1915 . . . 4 𝑧(𝑥𝐴𝜑)
2 cbvrabw.1 . . . . . 6 𝑥𝐴
32nfcri 2888 . . . . 5 𝑥 𝑧𝐴
4 nfs1v 2151 . . . . 5 𝑥[𝑧 / 𝑥]𝜑
53, 4nfan 1900 . . . 4 𝑥(𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)
6 eleq1w 2814 . . . . 5 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
7 sbequ12 2241 . . . . 5 (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
86, 7anbi12d 629 . . . 4 (𝑥 = 𝑧 → ((𝑥𝐴𝜑) ↔ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)))
91, 5, 8cbvabw 2804 . . 3 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑧 ∣ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)}
10 cbvrabw.2 . . . . . 6 𝑦𝐴
1110nfcri 2888 . . . . 5 𝑦 𝑧𝐴
12 cbvrabw.3 . . . . . 6 𝑦𝜑
1312nfsbv 2321 . . . . 5 𝑦[𝑧 / 𝑥]𝜑
1411, 13nfan 1900 . . . 4 𝑦(𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)
15 nfv 1915 . . . 4 𝑧(𝑦𝐴𝜓)
16 eleq1w 2814 . . . . 5 (𝑧 = 𝑦 → (𝑧𝐴𝑦𝐴))
17 sbequ 2084 . . . . . 6 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
18 cbvrabw.4 . . . . . . 7 𝑥𝜓
19 cbvrabw.5 . . . . . . 7 (𝑥 = 𝑦 → (𝜑𝜓))
2018, 19sbiev 2306 . . . . . 6 ([𝑦 / 𝑥]𝜑𝜓)
2117, 20bitrdi 286 . . . . 5 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑𝜓))
2216, 21anbi12d 629 . . . 4 (𝑧 = 𝑦 → ((𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑) ↔ (𝑦𝐴𝜓)))
2314, 15, 22cbvabw 2804 . . 3 {𝑧 ∣ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)} = {𝑦 ∣ (𝑦𝐴𝜓)}
249, 23eqtri 2758 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑦 ∣ (𝑦𝐴𝜓)}
25 df-rab 3431 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
26 df-rab 3431 . 2 {𝑦𝐴𝜓} = {𝑦 ∣ (𝑦𝐴𝜓)}
2724, 25, 263eqtr4i 2768 1 {𝑥𝐴𝜑} = {𝑦𝐴𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1539  wnf 1783  [wsb 2065  wcel 2104  {cab 2707  wnfc 2881  {crab 3430
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-rab 3431
This theorem is referenced by:  elrabsf  3824  f1ossf1o  7127  tfis  7846  cantnflem1  9686  scottexs  9884  scott0s  9885  elmptrab  23551  bnj1534  34162  scottexf  37339  scott0f  37340  eq0rabdioph  41816  rexrabdioph  41834  rexfrabdioph  41835  elnn0rabdioph  41843  dvdsrabdioph  41850  binomcxplemdvsum  43416  fnlimcnv  44681  fnlimabslt  44693  stoweidlem34  45048  stoweidlem59  45073  pimltmnf2f  45711  pimgtpnf2f  45719  pimltpnf2f  45726  issmff  45748  smfpimltxrmptf  45772  smfpreimagtf  45782  smflim  45791  smfpimgtxr  45794  smfpimgtxrmptf  45798  smflim2  45820  smflimsup  45842  smfliminf  45845
  Copyright terms: Public domain W3C validator