Theorem cbvrabv 3419

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 2158 and ax-13 2371. (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 2812	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2800	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3409	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3409	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2763	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {cab 2708  {crab 3408

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409

This theorem is referenced by:  rru  3753  knatar  7335  oeeulem  8568  cofon1  8639  ordtypecbv  9477  ordtypelem9  9486  inf3lema  9584  oemapso  9642  oemapvali  9644  tz9.12lem3  9749  cofsmo  10229  enfin2i  10281  fin23lem33  10305  isf32lem11  10323  zorn2g  10463  pwfseqlem1  10618  pwfseqlem3  10620  zsupss  12903  zmin  12910  rpnnen1  12949  hashbc  14425  wrd2f1tovbij  14933  01sqrexlem7  15221  divalglem5  16374  bitsfzolem  16411  smupp1  16457  gcdcllem3  16478  bezout  16520  eulerth  16760  odzval  16769  pcprecl  16817  pcprendvds  16818  pcpremul  16821  pceulem  16823  prmreclem1  16894  prmreclem5  16898  prmreclem6  16899  4sqlem19  16941  vdwnn  16976  hashbcval  16980  gsumvalx  18610  symgfixelq  19370  efgsdm  19667  efgsfo  19676  ablfaclem3  20026  ltbwe  21958  coe1mul2lem2  22161  smadiadetlem3  22562  pptbas  22902  conncompss  23327  ptcmplem5  23950  ustuqtop  24141  utopsnneip  24143  icccmplem2  24719  minveclem5  25340  ivth  25362  ovolicc2lem5  25429  ovolicc  25431  opnmbllem  25509  vitali  25521  itg2monolem3  25660  elqaa  26237  radcnvle  26336  pserdvlem2  26345  lgamgulmlem5  26950  lgamcvglem  26957  wilth  26988  ftalem6  26995  precsexlemcbv  28115  bdayon  28180  ttgval  28809  axcontlem11  28908  lfgredgge2  29058  usgredgleordALT  29168  nbusgrf1o  29305  cusgrexg  29378  cusgrfilem2  29391  cusgrfi  29393  vtxdushgrfvedglem  29424  vtxdushgrfvedg  29425  vtxdginducedm1  29478  finsumvtxdg2sstep  29484  wwlksnextbij  29839  rusgrnumwwlks  29911  clwlkclwwlkfolem  29943  clwlkclwwlken  29948  clwwlknscsh  29998  hashecclwwlkn1  30013  umgrhashecclwwlk  30014  clwlknf1oclwwlknlem2  30018  clwlknf1oclwwlkn  30020  frgrwopreglem5lem  30256  frgrregorufr0  30260  fusgreghash2wsp  30274  dlwwlknondlwlknonf1o  30301  ubthlem3  30808  htth  30854  fcobijfs  32653  elrgspnsubrunlem1  33205  elrgspnsubrun  33207  1arithufd  33526  constrsuc  33735  constrcbvlem  33752  locfinreflem  33837  zarmxt1  33877  zarcmp  33879  ordtconnlem1  33921  dynkin  34164  ddemeas  34233  oddpwdc  34352  eulerpartgbij  34370  eulerpartlemn  34379  eulerpart  34380  ballotlemelo  34486  ballotleme  34495  ballotlem7  34534  reprsuc  34613  hgt750lema  34655  hgt750leme  34656  onvf1odlem3  35099  subfacp1lem6  35179  erdsze  35196  cvmscbv  35252  cvmsiota  35271  cvmlift2lem13  35309  satfv1  35357  neibastop2  36356  weiunfrlem  36459  topdifinffin  37343  poimirlem27  37648  mblfinlem1  37658  mblfinlem2  37659  lclkrs2  41541  aks4d1  42084  sticksstones2  42142  eldioph4i  42807  rfovcnvf1od  44000  fsovrfovd  44005  fsovcnvlem  44009  nzss  44313  supminfxr2  45472  limcperiod  45633  cncfshiftioo  45897  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnprodlem1  45951  dvnprod  45954  itgiccshift  45985  itgperiod  45986  stoweidlem49  46054  fourierdlem41  46153  fourierdlem48  46159  fourierdlem49  46160  fourierdlem54  46165  fourierdlem65  46176  fourierdlem70  46181  fourierdlem71  46182  fourierdlem81  46192  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem92  46203  fourierdlem96  46207  fourierdlem97  46208  fourierdlem98  46209  fourierdlem99  46210  fourierdlem100  46211  fourierdlem103  46214  fourierdlem104  46215  fourierdlem105  46216  fourierdlem108  46219  fourierdlem109  46220  fourierdlem110  46221  fourierdlem112  46223  fourierdlem113  46224  elaa2  46239  etransclem11  46250  etransc  46288  salexct  46339  subsaliuncl  46363  sge0fodjrnlem  46421  meadjiun  46471  ovnsubadd  46577  hoidmv1le  46599  hoidmvlelem3  46602  hoidmvlelem5  46604  ovnhoi  46608  hspmbllem3  46633  hspmbl  46634  opnvonmbl  46639  ovolval4lem2  46655  ovolval5lem2  46658  ovolval5lem3  46659  ovolval5  46660  ovnovol  46664  issmf  46733  incsmf  46747  issmfle  46750  issmfgt  46761  smfadd  46770  decsmf  46772  issmfge  46775  smflimlem4  46779  smflim  46782  smfmul  46800  smflimsuplem2  46826  smflimsuplem5  46829  smflimsuplem7  46831  requad2  47628  uspgrlimlem1  47991  grlimgrtri  47999  gpgusgralem  48051  intubeu  48976  unilbeu  48977