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

Theorem cbvrabw 3471
Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. Version of cbvrab 3477 with a disjoint variable condition, which does not require ax-13 2375. (Contributed by Andrew Salmon, 11-Jul-2011.) Avoid ax-13 2375. (Revised by GG, 10-Jan-2024.) Avoid ax-10 2139. (Revised by Wolf Lammen, 19-Jul-2025.)
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
StepHypRef Expression
1 cbvrabw.2 . . . . 5 𝑦𝐴
21nfcri 2895 . . . 4 𝑦 𝑥𝐴
3 cbvrabw.3 . . . 4 𝑦𝜑
42, 3nfan 1897 . . 3 𝑦(𝑥𝐴𝜑)
5 cbvrabw.1 . . . . 5 𝑥𝐴
65nfcri 2895 . . . 4 𝑥 𝑦𝐴
7 cbvrabw.4 . . . 4 𝑥𝜓
86, 7nfan 1897 . . 3 𝑥(𝑦𝐴𝜓)
9 eleq1w 2822 . . . 4 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
10 cbvrabw.5 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
119, 10anbi12d 632 . . 3 (𝑥 = 𝑦 → ((𝑥𝐴𝜑) ↔ (𝑦𝐴𝜓)))
124, 8, 11cbvabw 2811 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑦 ∣ (𝑦𝐴𝜓)}
13 df-rab 3434 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
14 df-rab 3434 . 2 {𝑦𝐴𝜓} = {𝑦 ∣ (𝑦𝐴𝜓)}
1512, 13, 143eqtr4i 2773 1 {𝑥𝐴𝜑} = {𝑦𝐴𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wnf 1780  wcel 2106  {cab 2712  wnfc 2888  {crab 3433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-11 2155  ax-12 2175  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-rab 3434
This theorem is referenced by:  elrabsf  3840  f1ossf1o  7148  tfis  7876  cantnflem1  9727  scottexs  9925  scott0s  9926  elmptrab  23851  bnj1534  34846  scottexf  38155  scott0f  38156  aks6d1c7lem3  42164  unitscyglem3  42179  unitscyglem4  42180  eq0rabdioph  42764  rexrabdioph  42782  rexfrabdioph  42783  elnn0rabdioph  42791  dvdsrabdioph  42798  binomcxplemdvsum  44351  fnlimcnv  45623  fnlimabslt  45635  stoweidlem34  45990  stoweidlem59  46015  pimltmnf2f  46653  pimgtpnf2f  46661  pimltpnf2f  46668  issmff  46690  smfpimltxrmptf  46714  smfpreimagtf  46724  smflim  46733  smfpimgtxr  46736  smfpimgtxrmptf  46740  smflim2  46762  smflimsup  46784  smfliminf  46787
  Copyright terms: Public domain W3C validator