Theorem cbvrabv 3424

Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2157 and ax-13 2373. (Revised by Steven Nguyen, 4-Dec-2022.)

Hypothesis

Ref	Expression
cbvrabv.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvrabv	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvrabv

Step	Hyp	Ref	Expression
1		eleq1w 2822	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 630	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2812	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3074	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3074	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2777	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1541   ∈ wcel 2109  {cab 2716  {crab 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074

This theorem is referenced by:  rabrabiOLD  3426  rru  3717  knatar  7221  oeeulem  8408  ordtypecbv  9237  ordtypelem9  9246  inf3lema  9343  oemapso  9401  oemapvali  9403  tz9.12lem3  9531  cofsmo  10009  enfin2i  10061  fin23lem33  10085  isf32lem11  10103  zorn2g  10243  pwfseqlem1  10398  pwfseqlem3  10400  zsupss  12659  zmin  12666  rpnnen1  12705  hashbc  14146  wrd2f1tovbij  14656  sqrlem7  14941  divalglem5  16087  bitsfzolem  16122  smupp1  16168  gcdcllem3  16189  bezout  16232  eulerth  16465  odzval  16473  pcprecl  16521  pcprendvds  16522  pcpremul  16525  pceulem  16527  prmreclem1  16598  prmreclem5  16602  prmreclem6  16603  4sqlem19  16645  vdwnn  16680  hashbcval  16684  gsumvalx  18341  symgfixelq  19022  efgsdm  19317  efgsfo  19326  ablfaclem3  19671  ltbwe  21226  coe1mul2lem2  21420  smadiadetlem3  21798  pptbas  22139  conncompss  22565  ptcmplem5  23188  ustuqtop  23379  utopsnneip  23381  icccmplem2  23967  minveclem5  24578  ivth  24599  ovolicc2lem5  24666  ovolicc  24668  opnmbllem  24746  vitali  24758  itg2monolem3  24898  elqaa  25463  radcnvle  25560  pserdvlem2  25568  lgamgulmlem5  26163  lgamcvglem  26170  wilth  26201  ftalem6  26208  ttgval  27217  ttgvalOLD  27218  axcontlem11  27323  lfgredgge2  27475  usgredgleordALT  27582  nbusgrf1o  27719  cusgrexg  27792  cusgrfilem2  27804  cusgrfi  27806  vtxdushgrfvedglem  27837  vtxdushgrfvedg  27838  vtxdginducedm1  27891  finsumvtxdg2sstep  27897  wwlksnextbij  28246  rusgrnumwwlks  28318  clwlkclwwlkfolem  28350  clwlkclwwlken  28355  clwwlknscsh  28405  hashecclwwlkn1  28420  umgrhashecclwwlk  28421  clwlknf1oclwwlknlem2  28425  clwlknf1oclwwlkn  28427  frgrwopreglem5lem  28663  frgrregorufr0  28667  fusgreghash2wsp  28681  dlwwlknondlwlknonf1o  28708  ubthlem3  29213  htth  29259  fcobijfs  31037  locfinreflem  31769  zarmxt1  31809  zarcmp  31811  ordtconnlem1  31853  dynkin  32114  ddemeas  32183  oddpwdc  32300  eulerpartgbij  32318  eulerpartlemn  32327  eulerpart  32328  ballotlemelo  32433  ballotleme  32442  ballotlem7  32481  reprsuc  32574  hgt750lema  32616  hgt750leme  32617  subfacp1lem6  33126  erdsze  33143  cvmscbv  33199  cvmsiota  33218  cvmlift2lem13  33256  satfv1  33304  neibastop2  34529  topdifinffin  35498  poimirlem27  35783  mblfinlem1  35793  mblfinlem2  35794  lclkrs2  39533  aks4d1  40077  sticksstones2  40083  eldioph4i  40614  rfovcnvf1od  41565  fsovrfovd  41570  fsovcnvlem  41574  nzss  41888  supminfxr2  42963  limcperiod  43123  cncfshiftioo  43387  ioodvbdlimc1lem2  43427  ioodvbdlimc2lem  43429  dvnprodlem1  43441  dvnprod  43444  itgiccshift  43475  itgperiod  43476  stoweidlem49  43544  fourierdlem41  43643  fourierdlem48  43649  fourierdlem49  43650  fourierdlem54  43655  fourierdlem65  43666  fourierdlem70  43671  fourierdlem71  43672  fourierdlem81  43682  fourierdlem89  43690  fourierdlem90  43691  fourierdlem91  43692  fourierdlem92  43693  fourierdlem96  43697  fourierdlem97  43698  fourierdlem98  43699  fourierdlem99  43700  fourierdlem100  43701  fourierdlem103  43704  fourierdlem104  43705  fourierdlem105  43706  fourierdlem108  43709  fourierdlem109  43710  fourierdlem110  43711  fourierdlem112  43713  fourierdlem113  43714  elaa2  43729  etransclem11  43740  etransc  43778  salexct  43827  subsaliuncl  43851  sge0fodjrnlem  43908  meadjiun  43958  ovnsubadd  44064  hoidmv1le  44086  hoidmvlelem3  44089  hoidmvlelem5  44091  ovnhoi  44095  hspmbllem3  44120  hspmbl  44121  opnvonmbl  44126  ovolval4lem2  44142  ovolval5lem2  44145  ovolval5lem3  44146  ovolval5  44147  ovnovol  44151  issmf  44215  incsmf  44229  issmfle  44232  issmfgt  44243  smfadd  44251  decsmf  44253  issmfge  44256  smflimlem4  44260  smflim  44263  smfmul  44280  smflimsuplem2  44305  smflimsuplem5  44308  smflimsuplem7  44310  requad2  45027  intubeu  46222  unilbeu  46223