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

Theorem cbvrabw 3474
 Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. Version of cbvrab 3475 with a disjoint variable condition, which does not require ax-13 2392. (Contributed by Andrew Salmon, 11-Jul-2011.) (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 1916 . . . 4 𝑧(𝑥𝐴𝜑)
2 cbvrabw.1 . . . . . 6 𝑥𝐴
32nfcri 2971 . . . . 5 𝑥 𝑧𝐴
4 nfs1v 2161 . . . . 5 𝑥[𝑧 / 𝑥]𝜑
53, 4nfan 1901 . . . 4 𝑥(𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)
6 eleq1w 2898 . . . . 5 (𝑥 = 𝑧 → (𝑥𝐴𝑧𝐴))
7 sbequ12 2255 . . . . 5 (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
86, 7anbi12d 633 . . . 4 (𝑥 = 𝑧 → ((𝑥𝐴𝜑) ↔ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)))
91, 5, 8cbvabw 2893 . . 3 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑧 ∣ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)}
10 cbvrabw.2 . . . . . 6 𝑦𝐴
1110nfcri 2971 . . . . 5 𝑦 𝑧𝐴
12 cbvrabw.3 . . . . . 6 𝑦𝜑
1312nfsbv 2351 . . . . 5 𝑦[𝑧 / 𝑥]𝜑
1411, 13nfan 1901 . . . 4 𝑦(𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)
15 nfv 1916 . . . 4 𝑧(𝑦𝐴𝜓)
16 eleq1w 2898 . . . . 5 (𝑧 = 𝑦 → (𝑧𝐴𝑦𝐴))
17 sbequ 2091 . . . . . 6 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑))
18 cbvrabw.4 . . . . . . 7 𝑥𝜓
19 cbvrabw.5 . . . . . . 7 (𝑥 = 𝑦 → (𝜑𝜓))
2018, 19sbiev 2332 . . . . . 6 ([𝑦 / 𝑥]𝜑𝜓)
2117, 20syl6bb 290 . . . . 5 (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑𝜓))
2216, 21anbi12d 633 . . . 4 (𝑧 = 𝑦 → ((𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑) ↔ (𝑦𝐴𝜓)))
2314, 15, 22cbvabw 2893 . . 3 {𝑧 ∣ (𝑧𝐴 ∧ [𝑧 / 𝑥]𝜑)} = {𝑦 ∣ (𝑦𝐴𝜓)}
249, 23eqtri 2847 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑦 ∣ (𝑦𝐴𝜓)}
25 df-rab 3141 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
26 df-rab 3141 . 2 {𝑦𝐴𝜓} = {𝑦 ∣ (𝑦𝐴𝜓)}
2724, 25, 263eqtr4i 2857 1 {𝑥𝐴𝜑} = {𝑦𝐴𝜓}
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  Ⅎwnf 1785  [wsb 2070   ∈ wcel 2115  {cab 2802  Ⅎwnfc 2962  {crab 3136 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-rab 3141 This theorem is referenced by:  elrabsf  3801  f1ossf1o  6871  tfis  7552  cantnflem1  9136  scottexs  9300  scott0s  9301  elmptrab  22421  bnj1534  32143  scottexf  35506  scott0f  35507  eq0rabdioph  39549  rexrabdioph  39567  rexfrabdioph  39568  elnn0rabdioph  39576  dvdsrabdioph  39583  binomcxplemdvsum  40895  fnlimcnv  42151  fnlimabslt  42163  stoweidlem34  42518  stoweidlem59  42543  pimltmnf2  43178  pimgtpnf2  43184  pimltpnf2  43190  issmff  43210  smfpimltxrmpt  43234  smfpreimagtf  43243  smflim  43252  smfpimgtxr  43255  smfpimgtxrmpt  43259  smflim2  43279  smflimsup  43301  smfliminf  43304
 Copyright terms: Public domain W3C validator