Theorem cbvrabv 3399

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 2163 and ax-13 2376. (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 633	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2806	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3390	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3390	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2769	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {cab 2714  {crab 3389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390

This theorem is referenced by:  rru  3725  knatar  7312  oeeulem  8537  cofon1  8608  ordtypecbv  9432  ordtypelem9  9441  inf3lema  9545  oemapso  9603  oemapvali  9605  tz9.12lem3  9713  cofsmo  10191  enfin2i  10243  fin23lem33  10267  isf32lem11  10285  zorn2g  10425  pwfseqlem1  10581  pwfseqlem3  10583  zsupss  12887  zmin  12894  rpnnen1  12933  hashbc  14415  wrd2f1tovbij  14922  01sqrexlem7  15210  divalglem5  16366  bitsfzolem  16403  smupp1  16449  gcdcllem3  16470  bezout  16512  eulerth  16753  odzval  16762  pcprecl  16810  pcprendvds  16811  pcpremul  16814  pceulem  16816  prmreclem1  16887  prmreclem5  16891  prmreclem6  16892  4sqlem19  16934  vdwnn  16969  hashbcval  16973  gsumvalx  18644  symgfixelq  19408  efgsdm  19705  efgsfo  19714  ablfaclem3  20064  ltbwe  22022  coe1mul2lem2  22233  smadiadetlem3  22633  pptbas  22973  conncompss  23398  ptcmplem5  24021  ustuqtop  24211  utopsnneip  24213  icccmplem2  24789  minveclem5  25400  ivth  25421  ovolicc2lem5  25488  ovolicc  25490  opnmbllem  25568  vitali  25580  itg2monolem3  25719  elqaa  26288  radcnvle  26385  pserdvlem2  26393  lgamgulmlem5  26996  lgamcvglem  27003  wilth  27034  ftalem6  27041  precsexlemcbv  28198  bdayons  28268  ttgval  28943  axcontlem11  29043  lfgredgge2  29193  usgredgleordALT  29303  nbusgrf1o  29440  cusgrexg  29513  cusgrfilem2  29525  cusgrfi  29527  vtxdushgrfvedglem  29558  vtxdushgrfvedg  29559  vtxdginducedm1  29612  finsumvtxdg2sstep  29618  wwlksnextbij  29970  rusgrnumwwlks  30045  clwlkclwwlkfolem  30077  clwlkclwwlken  30082  clwwlknscsh  30132  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  clwlknf1oclwwlknlem2  30152  clwlknf1oclwwlkn  30154  frgrwopreglem5lem  30390  frgrregorufr0  30394  fusgreghash2wsp  30408  dlwwlknondlwlknonf1o  30435  ubthlem3  30943  htth  30989  fcobijfs  32794  fcobijfs2  32795  elrgspnsubrunlem1  33308  elrgspnsubrun  33310  1arithufd  33608  extvfvcl  33680  mplvrpmfgalem  33688  constrsuc  33882  constrcbvlem  33899  locfinreflem  33984  zarmxt1  34024  zarcmp  34026  ordtconnlem1  34068  dynkin  34311  ddemeas  34380  oddpwdc  34498  eulerpartgbij  34516  eulerpartlemn  34525  eulerpart  34526  ballotlemelo  34632  ballotleme  34641  ballotlem7  34680  reprsuc  34759  hgt750lema  34801  hgt750leme  34802  fineqvnttrclse  35268  onvf1odlem3  35287  subfacp1lem6  35367  erdsze  35384  cvmscbv  35440  cvmsiota  35459  cvmlift2lem13  35497  satfv1  35545  neibastop2  36543  weiunfrlem  36646  topdifinffin  37664  poimirlem27  37968  mblfinlem1  37978  mblfinlem2  37979  lclkrs2  41986  aks4d1  42528  sticksstones2  42586  eldioph4i  43240  rfovcnvf1od  44431  fsovrfovd  44436  fsovcnvlem  44440  nzss  44744  supminfxr2  45897  limcperiod  46058  cncfshiftioo  46320  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnprodlem1  46374  dvnprod  46377  itgiccshift  46408  itgperiod  46409  stoweidlem49  46477  fourierdlem41  46576  fourierdlem48  46582  fourierdlem49  46583  fourierdlem54  46588  fourierdlem65  46599  fourierdlem70  46604  fourierdlem71  46605  fourierdlem81  46615  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem92  46626  fourierdlem96  46630  fourierdlem97  46631  fourierdlem98  46632  fourierdlem99  46633  fourierdlem100  46634  fourierdlem103  46637  fourierdlem104  46638  fourierdlem105  46639  fourierdlem108  46642  fourierdlem109  46643  fourierdlem110  46644  fourierdlem112  46646  fourierdlem113  46647  elaa2  46662  etransclem11  46673  etransc  46711  salexct  46762  subsaliuncl  46786  sge0fodjrnlem  46844  meadjiun  46894  ovnsubadd  47000  hoidmv1le  47022  hoidmvlelem3  47025  hoidmvlelem5  47027  ovnhoi  47031  hspmbllem3  47056  hspmbl  47057  opnvonmbl  47062  ovolval4lem2  47078  ovolval5lem2  47081  ovolval5lem3  47082  ovolval5  47083  ovnovol  47087  issmf  47156  incsmf  47170  issmfle  47173  issmfgt  47184  smfadd  47193  decsmf  47195  issmfge  47198  smflimlem4  47202  smflim  47205  smfmul  47223  smflimsuplem2  47249  smflimsuplem5  47252  smflimsuplem7  47254  requad2  48099  uspgrlimlem1  48464  grlimedgclnbgr  48471  grlimgrtri  48479  gpgusgralem  48532  intubeu  49459  unilbeu  49460