Theorem cbvrabv 3423

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 2190 and ax-13 2402. (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 2844	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 641	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2831	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3414	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3414	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2794	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559   ∈ wcel 2141  {cab 2739  {crab 3413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414

This theorem is referenced by:  rru  3740  knatar  7335  oeeulem  8564  cofon1  8635  ordtypecbv  9458  ordtypelem9  9467  inf3lema  9572  oemapso  9630  oemapvali  9632  tz9.12lem3  9740  cofsmo  10219  enfin2i  10271  fin23lem33  10295  isf32lem11  10313  zorn2g  10453  pwfseqlem1  10609  pwfseqlem3  10611  zsupss  12931  zmin  12938  rpnnen1  12977  hashbc  14459  wrd2f1tovbij  14966  01sqrexlem7  15265  divalglem5  16421  bitsfzolem  16458  smupp1  16504  gcdcllem3  16525  bezout  16567  eulerth  16808  odzval  16817  pcprecl  16865  pcprendvds  16866  pcpremul  16869  pceulem  16871  prmreclem1  16942  prmreclem5  16946  prmreclem6  16947  4sqlem19  16989  vdwnn  17024  hashbcval  17028  gsumvalx  18700  symgfixelq  19463  efgsdm  19760  efgsfo  19769  ablfaclem3  20119  ltbwe  22084  coe1mul2lem2  22318  smadiadetlem3  22715  pptbas  23055  conncompss  23480  ptcmplem5  24103  ustuqtop  24293  utopsnneip  24295  icccmplem2  24871  minveclem5  25482  ivth  25503  ovolicc2lem5  25570  ovolicc  25572  opnmbllem  25650  vitali  25662  itg2monolem3  25801  elqaa  26373  radcnvle  26470  pserdvlem2  26478  lgamgulmlem5  27084  lgamcvglem  27091  wilth  27122  ftalem6  27129  precsexlemcbv  28286  bdayons  28356  ttgval  29031  axcontlem11  29131  lfgredgge2  29281  usgredgleordALT  29391  nbusgrf1o  29528  cusgrexg  29601  cusgrfilem2  29613  cusgrfi  29615  vtxdushgrfvedglem  29646  vtxdushgrfvedg  29647  vtxdginducedm1  29700  finsumvtxdg2sstep  29706  wwlksnextbij  30058  rusgrnumwwlks  30133  clwlkclwwlkfolem  30165  clwlkclwwlken  30170  clwwlknscsh  30220  hashecclwwlkn1  30235  umgrhashecclwwlk  30236  clwlknf1oclwwlknlem2  30240  clwlknf1oclwwlkn  30242  frgrwopreglem5lem  30478  frgrregorufr0  30482  fusgreghash2wsp  30496  dlwwlknondlwlknonf1o  30523  ubthlem3  31031  htth  31077  fcobijfs  32883  fcobijfs2  32884  elrgspnsubrunlem1  33388  elrgspnsubrun  33390  1arithufd  33704  extvfvcl  33793  mplvrpmfgalem  33801  constrsuc  33995  constrcbvlem  34012  locfinreflem  34097  zarmxt1  34137  zarcmp  34139  ordtconnlem1  34181  dynkin  34424  ddemeas  34493  oddpwdc  34611  eulerpartgbij  34629  eulerpartlemn  34638  eulerpart  34639  ballotlemelo  34745  ballotleme  34754  ballotlem7  34793  reprsuc  34869  hgt750lema  34911  hgt750leme  34912  fineqvnttrclse  35380  onvf1odlem3  35408  subfacp1lem6  35495  erdsze  35512  cvmscbv  35568  cvmsiota  35587  cvmlift2lem13  35625  satfv1  35673  neibastop2  36681  weiunfrlem  36784  topdifinffin  37802  poimirlem27  38106  mblfinlem1  38116  mblfinlem2  38117  lclkrs2  42124  aks4d1  42666  sticksstones2  42724  eldioph4i  43349  rfovcnvf1od  44540  fsovrfovd  44545  fsovcnvlem  44549  nzss  44853  supminfxr2  46003  limcperiod  46164  cncfshiftioo  46426  ioodvbdlimc1lem2  46466  ioodvbdlimc2lem  46468  dvnprodlem1  46480  dvnprod  46483  itgiccshift  46514  itgperiod  46515  stoweidlem49  46583  fourierdlem41  46682  fourierdlem48  46688  fourierdlem49  46689  fourierdlem54  46694  fourierdlem65  46705  fourierdlem70  46710  fourierdlem71  46711  fourierdlem81  46721  fourierdlem89  46729  fourierdlem90  46730  fourierdlem91  46731  fourierdlem92  46732  fourierdlem96  46736  fourierdlem97  46737  fourierdlem98  46738  fourierdlem99  46739  fourierdlem100  46740  fourierdlem103  46743  fourierdlem104  46744  fourierdlem105  46745  fourierdlem108  46748  fourierdlem109  46749  fourierdlem110  46750  fourierdlem112  46752  fourierdlem113  46753  elaa2  46768  etransclem11  46779  etransc  46817  salexct  46868  subsaliuncl  46892  sge0fodjrnlem  46950  meadjiun  47000  ovnsubadd  47106  hoidmv1le  47128  hoidmvlelem3  47131  hoidmvlelem5  47133  ovnhoi  47137  hspmbllem3  47162  hspmbl  47163  opnvonmbl  47168  ovolval4lem2  47184  ovolval5lem2  47187  ovolval5lem3  47188  ovolval5  47189  ovnovol  47193  issmf  47262  incsmf  47276  issmfle  47279  issmfgt  47290  smfadd  47299  decsmf  47301  issmfge  47304  smflimlem4  47308  smflim  47311  smfmul  47329  smflimsuplem2  47355  smflimsuplem5  47358  smflimsuplem7  47360  requad2  48205  uspgrlimlem1  48570  grlimedgclnbgr  48577  grlimgrtri  48585  gpgusgralem  48638  intubeu  49565  unilbeu  49566