Theorem cbvrabv 3422

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 2193 and ax-13 2401. (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 2843	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 644	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2830	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3413	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3413	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2793	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {cab 2738  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413

This theorem is used by:  rru  3736  knatar  7368  oeeulem  8614  cofon1  8685  ordtypecbv  9515  ordtypelem9  9524  inf3lema  9629  oemapso  9687  oemapvali  9689  tz9.12lem3  9800  cofsmo  10351  enfin2i  10403  fin23lem33  10427  isf32lem11  10445  zorn2g  10585  pwfseqlem1  10747  pwfseqlem3  10749  zsupss  13068  zmin  13075  rpnnen1  13115  hashbc  14602  wrd2f1tovbij  15119  01sqrexlem7  15421  divalglem5  16573  bitsfzolem  16610  smupp1  16656  gcdcllem3  16677  bezout  16722  eulerth  16966  odzval  16975  pcprecl  17023  pcprendvds  17024  pcpremul  17027  pceulem  17029  prmreclem1  17100  prmreclem5  17104  prmreclem6  17105  4sqlem19  17147  vdwnn  17182  hashbcval  17186  gsumvalx  18871  symgfixelq  19653  efgsdm  19950  efgsfo  19959  ablfaclem3  20309  ltbwe  22359  coe1mul2lem2  22593  smadiadetlem3  22989  pptbas  23332  conncompss  23757  ptcmplem5  24381  ustuqtop  24571  utopsnneip  24573  icccmplem2  25149  minveclem5  25760  ivth  25781  ovolicc2lem5  25848  ovolicc  25850  opnmbllem  25928  vitali  25940  itg2monolem3  26079  elqaa  26651  radcnvle  26753  pserdvlem2  26761  lgamgulmlem5  27366  lgamcvglem  27373  wilth  27404  ftalem6  27411  precsexlemcbv  28598  bdayons  28668  ttgval  29458  axcontlem11  29558  lfgredgge2  29708  usgredgleordALT  29821  nbusgrf1o  29958  cusgrexg  30031  cusgrfilem2  30043  cusgrfi  30045  vtxdushgrfvedglem  30076  vtxdushgrfvedg  30077  vtxdginducedm1  30130  finsumvtxdg2sstep  30136  wwlksnextbij  30497  rusgrnumwwlks  30572  clwlkclwwlkfolem  30604  clwlkclwwlken  30609  clwwlknscsh  30659  hashecclwwlkn1  30674  umgrhashecclwwlk  30675  clwlknf1oclwwlknlem2  30679  clwlknf1oclwwlkn  30681  frgrwopreglem5lem  30927  frgrregorufr0  30931  fusgreghash2wsp  30945  dlwwlknondlwlknonf1o  30972  ubthlem3  31480  htth  31526  fcobijfs  33360  fcobijfs2  33361  elrgspnsubrunlem1  33855  elrgspnsubrun  33857  1arithufd  34127  extvfvcl  34215  mplvrpmfgalem  34223  constrsuc  34417  constrcbvlem  34434  locfinreflem  34519  zarmxt1  34559  zarcmp  34561  ordtconnlem1  34603  dynkin  34847  ddemeas  34916  oddpwdc  35033  eulerpartgbij  35051  eulerpartlemn  35060  eulerpart  35061  ballotlemelo  35167  ballotleme  35176  ballotlem7  35215  reprsuc  35291  hgt750lema  35333  hgt750leme  35334  werankwe  35792  werankwe2  35793  fineqvnttrclse  35849  onvf1odlem3  35953  subfacp1lem6  36037  erdsze  36054  cvmscbv  36110  cvmsiota  36129  cvmlift2lem13  36167  satfv1  36215  cardprcALT  36552  neibastop2  37242  weiunfrlem  37345  topdifinffin  38365  poimirlem27  38659  mblfinlem1  38669  mblfinlem2  38670  lclkrs2  42691  aks4d1  43233  sticksstones2  43291  eldioph4i  43913  rfovcnvf1od  45098  fsovrfovd  45103  fsovcnvlem  45107  nzss  45395  supminfxr2  46573  limcperiod  46734  cncfshiftioo  46996  ioodvbdlimc1lem2  47036  ioodvbdlimc2lem  47038  dvnprodlem1  47050  dvnprod  47053  itgiccshift  47084  itgperiod  47085  stoweidlem49  47153  fourierdlem41  47252  fourierdlem48  47258  fourierdlem49  47259  fourierdlem54  47264  fourierdlem65  47275  fourierdlem70  47280  fourierdlem71  47281  fourierdlem81  47291  fourierdlem89  47299  fourierdlem90  47300  fourierdlem91  47301  fourierdlem92  47302  fourierdlem96  47306  fourierdlem97  47307  fourierdlem98  47308  fourierdlem99  47309  fourierdlem100  47310  fourierdlem103  47313  fourierdlem104  47314  fourierdlem105  47315  fourierdlem108  47318  fourierdlem109  47319  fourierdlem110  47320  fourierdlem112  47322  fourierdlem113  47323  elaa2  47338  etransclem11  47349  etransc  47387  salexct  47438  subsaliuncl  47462  sge0fodjrnlem  47520  meadjiun  47570  ovnsubadd  47676  hoidmv1le  47698  hoidmvlelem3  47701  hoidmvlelem5  47703  ovnhoi  47707  hspmbllem3  47732  hspmbl  47733  opnvonmbl  47738  ovolval4lem2  47754  ovolval5lem2  47757  ovolval5lem3  47758  ovolval5  47759  ovnovol  47763  issmf  47832  incsmf  47846  issmfle  47849  issmfgt  47860  smfadd  47869  decsmf  47871  issmfge  47874  smflimlem4  47878  smflim  47881  smfmul  47899  smflimsuplem2  47925  smflimsuplem5  47928  smflimsuplem7  47930  requad2  48815  uspgrlimlem1  49180  grlimedgclnbgr  49187  grlimgrtri  49195  gpgusgralem  49248  intubeu  50192  unilbeu  50193