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 2194 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 1570   ∈ wcel 2145  {cab 2738  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

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

This theorem is used by:  rru  3737  knatar  7360  oeeulem  8589  cofon1  8660  ordtypecbv  9489  ordtypelem9  9498  inf3lema  9603  oemapso  9661  oemapvali  9663  tz9.12lem3  9771  cofsmo  10271  enfin2i  10323  fin23lem33  10347  isf32lem11  10365  zorn2g  10505  pwfseqlem1  10667  pwfseqlem3  10669  zsupss  12986  zmin  12993  rpnnen1  13033  hashbc  14518  wrd2f1tovbij  15033  01sqrexlem7  15335  divalglem5  16487  bitsfzolem  16524  smupp1  16570  gcdcllem3  16591  bezout  16633  eulerth  16874  odzval  16883  pcprecl  16931  pcprendvds  16932  pcpremul  16935  pceulem  16937  prmreclem1  17008  prmreclem5  17012  prmreclem6  17013  4sqlem19  17055  vdwnn  17090  hashbcval  17094  gsumvalx  18778  symgfixelq  19560  efgsdm  19857  efgsfo  19866  ablfaclem3  20216  ltbwe  22260  coe1mul2lem2  22494  smadiadetlem3  22890  pptbas  23233  conncompss  23658  ptcmplem5  24282  ustuqtop  24472  utopsnneip  24474  icccmplem2  25050  minveclem5  25661  ivth  25682  ovolicc2lem5  25749  ovolicc  25751  opnmbllem  25829  vitali  25841  itg2monolem3  25980  elqaa  26554  radcnvle  26656  pserdvlem2  26664  lgamgulmlem5  27269  lgamcvglem  27276  wilth  27307  ftalem6  27314  precsexlemcbv  28471  bdayons  28541  ttgval  29331  axcontlem11  29431  lfgredgge2  29581  usgredgleordALT  29694  nbusgrf1o  29831  cusgrexg  29904  cusgrfilem2  29916  cusgrfi  29918  vtxdushgrfvedglem  29949  vtxdushgrfvedg  29950  vtxdginducedm1  30003  finsumvtxdg2sstep  30009  wwlksnextbij  30370  rusgrnumwwlks  30445  clwlkclwwlkfolem  30477  clwlkclwwlken  30482  clwwlknscsh  30532  hashecclwwlkn1  30547  umgrhashecclwwlk  30548  clwlknf1oclwwlknlem2  30552  clwlknf1oclwwlkn  30554  frgrwopreglem5lem  30800  frgrregorufr0  30804  fusgreghash2wsp  30818  dlwwlknondlwlknonf1o  30845  ubthlem3  31353  htth  31399  fcobijfs  33192  fcobijfs2  33193  elrgspnsubrunlem1  33687  elrgspnsubrun  33689  1arithufd  33958  extvfvcl  34046  mplvrpmfgalem  34054  constrsuc  34248  constrcbvlem  34265  locfinreflem  34350  zarmxt1  34390  zarcmp  34392  ordtconnlem1  34434  dynkin  34678  ddemeas  34747  oddpwdc  34865  eulerpartgbij  34883  eulerpartlemn  34892  eulerpart  34893  ballotlemelo  34999  ballotleme  35008  ballotlem7  35047  reprsuc  35123  hgt750lema  35165  hgt750leme  35166  fineqvnttrclse  35650  onvf1odlem3  35702  subfacp1lem6  35764  erdsze  35781  cvmscbv  35837  cvmsiota  35856  cvmlift2lem13  35894  satfv1  35942  neibastop2  36980  weiunfrlem  37083  topdifinffin  38102  poimirlem27  38396  mblfinlem1  38406  mblfinlem2  38407  lclkrs2  42413  aks4d1  42955  sticksstones2  43013  eldioph4i  43653  rfovcnvf1od  44844  fsovrfovd  44849  fsovcnvlem  44853  nzss  45141  supminfxr2  46297  limcperiod  46458  cncfshiftioo  46720  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  dvnprodlem1  46774  dvnprod  46777  itgiccshift  46808  itgperiod  46809  stoweidlem49  46877  fourierdlem41  46976  fourierdlem48  46982  fourierdlem49  46983  fourierdlem54  46988  fourierdlem65  46999  fourierdlem70  47004  fourierdlem71  47005  fourierdlem81  47015  fourierdlem89  47023  fourierdlem90  47024  fourierdlem91  47025  fourierdlem92  47026  fourierdlem96  47030  fourierdlem97  47031  fourierdlem98  47032  fourierdlem99  47033  fourierdlem100  47034  fourierdlem103  47037  fourierdlem104  47038  fourierdlem105  47039  fourierdlem108  47042  fourierdlem109  47043  fourierdlem110  47044  fourierdlem112  47046  fourierdlem113  47047  elaa2  47062  etransclem11  47073  etransc  47111  salexct  47162  subsaliuncl  47186  sge0fodjrnlem  47244  meadjiun  47294  ovnsubadd  47400  hoidmv1le  47422  hoidmvlelem3  47425  hoidmvlelem5  47427  ovnhoi  47431  hspmbllem3  47456  hspmbl  47457  opnvonmbl  47462  ovolval4lem2  47478  ovolval5lem2  47481  ovolval5lem3  47482  ovolval5  47483  ovnovol  47487  issmf  47556  incsmf  47570  issmfle  47573  issmfgt  47584  smfadd  47593  decsmf  47595  issmfge  47598  smflimlem4  47602  smflim  47605  smfmul  47623  smflimsuplem2  47649  smflimsuplem5  47652  smflimsuplem7  47654  requad2  48539  uspgrlimlem1  48904  grlimedgclnbgr  48911  grlimgrtri  48919  gpgusgralem  48972  intubeu  49910  unilbeu  49911