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

Theorem cbvrabw 3473
Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. Version of cbvrab 3479 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by Andrew Salmon, 11-Jul-2011.) Avoid ax-13 2377. (Revised by GG, 10-Jan-2024.) Avoid ax-10 2141. (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 2897 . . . 4 𝑦 𝑥𝐴
3 cbvrabw.3 . . . 4 𝑦𝜑
42, 3nfan 1899 . . 3 𝑦(𝑥𝐴𝜑)
5 cbvrabw.1 . . . . 5 𝑥𝐴
65nfcri 2897 . . . 4 𝑥 𝑦𝐴
7 cbvrabw.4 . . . 4 𝑥𝜓
86, 7nfan 1899 . . 3 𝑥(𝑦𝐴𝜓)
9 eleq1w 2824 . . . 4 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
10 cbvrabw.5 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
119, 10anbi12d 632 . . 3 (𝑥 = 𝑦 → ((𝑥𝐴𝜑) ↔ (𝑦𝐴𝜓)))
124, 8, 11cbvabw 2813 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑦 ∣ (𝑦𝐴𝜓)}
13 df-rab 3437 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
14 df-rab 3437 . 2 {𝑦𝐴𝜓} = {𝑦 ∣ (𝑦𝐴𝜓)}
1512, 13, 143eqtr4i 2775 1 {𝑥𝐴𝜑} = {𝑦𝐴𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wnf 1783  wcel 2108  {cab 2714  wnfc 2890  {crab 3436
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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-11 2157  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-rab 3437
This theorem is referenced by:  elrabsf  3834  f1ossf1o  7148  tfis  7876  cantnflem1  9729  scottexs  9927  scott0s  9928  elmptrab  23835  bnj1534  34867  scottexf  38175  scott0f  38176  aks6d1c7lem3  42183  unitscyglem3  42198  unitscyglem4  42199  eq0rabdioph  42787  rexrabdioph  42805  rexfrabdioph  42806  elnn0rabdioph  42814  dvdsrabdioph  42821  binomcxplemdvsum  44374  fnlimcnv  45682  fnlimabslt  45694  stoweidlem34  46049  stoweidlem59  46074  pimltmnf2f  46712  pimgtpnf2f  46720  pimltpnf2f  46727  issmff  46749  smfpimltxrmptf  46773  smfpreimagtf  46783  smflim  46792  smfpimgtxr  46795  smfpimgtxrmptf  46799  smflim2  46821  smflimsup  46843  smfliminf  46846
  Copyright terms: Public domain W3C validator