Theorem cbvrabv 3433

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 2152 and ax-13 2370. (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 2819	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2809	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3287	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3287	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2774	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1539   ∈ wcel 2104  {cab 2713  {crab 3284

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-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3287

This theorem is referenced by:  rabrabiOLD  3435  rru  3719  knatar  7260  oeeulem  8463  ordtypecbv  9320  ordtypelem9  9329  inf3lema  9426  oemapso  9484  oemapvali  9486  tz9.12lem3  9591  cofsmo  10071  enfin2i  10123  fin23lem33  10147  isf32lem11  10165  zorn2g  10305  pwfseqlem1  10460  pwfseqlem3  10462  zsupss  12723  zmin  12730  rpnnen1  12769  hashbc  14210  wrd2f1tovbij  14720  sqrlem7  15005  divalglem5  16151  bitsfzolem  16186  smupp1  16232  gcdcllem3  16253  bezout  16296  eulerth  16529  odzval  16537  pcprecl  16585  pcprendvds  16586  pcpremul  16589  pceulem  16591  prmreclem1  16662  prmreclem5  16666  prmreclem6  16667  4sqlem19  16709  vdwnn  16744  hashbcval  16748  gsumvalx  18405  symgfixelq  19086  efgsdm  19381  efgsfo  19390  ablfaclem3  19735  ltbwe  21290  coe1mul2lem2  21484  smadiadetlem3  21862  pptbas  22203  conncompss  22629  ptcmplem5  23252  ustuqtop  23443  utopsnneip  23445  icccmplem2  24031  minveclem5  24642  ivth  24663  ovolicc2lem5  24730  ovolicc  24732  opnmbllem  24810  vitali  24822  itg2monolem3  24962  elqaa  25527  radcnvle  25624  pserdvlem2  25632  lgamgulmlem5  26227  lgamcvglem  26234  wilth  26265  ftalem6  26272  ttgval  27281  ttgvalOLD  27282  axcontlem11  27387  lfgredgge2  27539  usgredgleordALT  27646  nbusgrf1o  27783  cusgrexg  27856  cusgrfilem2  27868  cusgrfi  27870  vtxdushgrfvedglem  27901  vtxdushgrfvedg  27902  vtxdginducedm1  27955  finsumvtxdg2sstep  27961  wwlksnextbij  28312  rusgrnumwwlks  28384  clwlkclwwlkfolem  28416  clwlkclwwlken  28421  clwwlknscsh  28471  hashecclwwlkn1  28486  umgrhashecclwwlk  28487  clwlknf1oclwwlknlem2  28491  clwlknf1oclwwlkn  28493  frgrwopreglem5lem  28729  frgrregorufr0  28733  fusgreghash2wsp  28747  dlwwlknondlwlknonf1o  28774  ubthlem3  29279  htth  29325  fcobijfs  31103  locfinreflem  31835  zarmxt1  31875  zarcmp  31877  ordtconnlem1  31919  dynkin  32180  ddemeas  32249  oddpwdc  32366  eulerpartgbij  32384  eulerpartlemn  32393  eulerpart  32394  ballotlemelo  32499  ballotleme  32508  ballotlem7  32547  reprsuc  32640  hgt750lema  32682  hgt750leme  32683  subfacp1lem6  33192  erdsze  33209  cvmscbv  33265  cvmsiota  33284  cvmlift2lem13  33322  satfv1  33370  neibastop2  34595  topdifinffin  35563  poimirlem27  35848  mblfinlem1  35858  mblfinlem2  35859  lclkrs2  39596  aks4d1  40139  sticksstones2  40145  eldioph4i  40671  rfovcnvf1od  41650  fsovrfovd  41655  fsovcnvlem  41659  nzss  41973  supminfxr2  43057  limcperiod  43218  cncfshiftioo  43482  ioodvbdlimc1lem2  43522  ioodvbdlimc2lem  43524  dvnprodlem1  43536  dvnprod  43539  itgiccshift  43570  itgperiod  43571  stoweidlem49  43639  fourierdlem41  43738  fourierdlem48  43744  fourierdlem49  43745  fourierdlem54  43750  fourierdlem65  43761  fourierdlem70  43766  fourierdlem71  43767  fourierdlem81  43777  fourierdlem89  43785  fourierdlem90  43786  fourierdlem91  43787  fourierdlem92  43788  fourierdlem96  43792  fourierdlem97  43793  fourierdlem98  43794  fourierdlem99  43795  fourierdlem100  43796  fourierdlem103  43799  fourierdlem104  43800  fourierdlem105  43801  fourierdlem108  43804  fourierdlem109  43805  fourierdlem110  43806  fourierdlem112  43808  fourierdlem113  43809  elaa2  43824  etransclem11  43835  etransc  43873  salexct  43922  subsaliuncl  43946  sge0fodjrnlem  44004  meadjiun  44054  ovnsubadd  44160  hoidmv1le  44182  hoidmvlelem3  44185  hoidmvlelem5  44187  ovnhoi  44191  hspmbllem3  44216  hspmbl  44217  opnvonmbl  44222  ovolval4lem2  44238  ovolval5lem2  44241  ovolval5lem3  44242  ovolval5  44243  ovnovol  44247  issmf  44316  incsmf  44330  issmfle  44333  issmfgt  44344  smfadd  44353  decsmf  44355  issmfge  44358  smflimlem4  44362  smflim  44365  smfmul  44383  smflimsuplem2  44408  smflimsuplem5  44411  smflimsuplem7  44413  requad2  45133  intubeu  46328  unilbeu  46329