Theorem cbvrabv 3491

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 2161 and ax-13 2390. (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 2895	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2889	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3147	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3147	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2854	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  {cab 2799  {crab 3142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147

This theorem is referenced by:  rabrabi  3493  rru  3770  knatar  7110  oeeulem  8227  ordtypecbv  8981  ordtypelem9  8990  inf3lema  9087  oemapso  9145  oemapvali  9147  tz9.12lem3  9218  cofsmo  9691  enfin2i  9743  fin23lem33  9767  isf32lem11  9785  zorn2g  9925  pwfseqlem1  10080  pwfseqlem3  10082  zsupss  12338  zmin  12345  rpnnen1  12383  hashbc  13812  wrd2f1tovbij  14324  sqrlem7  14608  divalglem5  15748  bitsfzolem  15783  smupp1  15829  gcdcllem3  15850  bezout  15891  eulerth  16120  odzval  16128  pcprecl  16176  pcprendvds  16177  pcpremul  16180  pceulem  16182  prmreclem1  16252  prmreclem5  16256  prmreclem6  16257  4sqlem19  16299  vdwnn  16334  hashbcval  16338  gsumvalx  17886  symgfixelq  18561  efgsdm  18856  efgsfo  18865  ablfaclem3  19209  ltbwe  20253  coe1mul2lem2  20436  smadiadetlem3  21277  pptbas  21616  conncompss  22041  ptcmplem5  22664  ustuqtop  22855  utopsnneip  22857  icccmplem2  23431  minveclem5  24036  ivth  24055  ovolicc2lem5  24122  ovolicc  24124  opnmbllem  24202  vitali  24214  itg2monolem3  24353  elqaa  24911  radcnvle  25008  pserdvlem2  25016  lgamgulmlem5  25610  lgamcvglem  25617  wilth  25648  ftalem6  25655  ttgval  26661  axcontlem11  26760  lfgredgge2  26909  usgredgleordALT  27016  nbusgrf1o  27153  cusgrexg  27226  cusgrfilem2  27238  cusgrfi  27240  vtxdushgrfvedglem  27271  vtxdushgrfvedg  27272  vtxdginducedm1  27325  finsumvtxdg2sstep  27331  wwlksnextbij  27680  rusgrnumwwlks  27753  clwlkclwwlkfolem  27785  clwlkclwwlken  27790  clwwlknscsh  27841  hashecclwwlkn1  27856  umgrhashecclwwlk  27857  clwlknf1oclwwlknlem2  27861  clwlknf1oclwwlkn  27863  frgrwopreglem5lem  28099  frgrregorufr0  28103  fusgreghash2wsp  28117  dlwwlknondlwlknonf1o  28144  ubthlem3  28649  htth  28695  fcobijfs  30459  locfinreflem  31104  ordtconnlem1  31167  dynkin  31426  ddemeas  31495  oddpwdc  31612  eulerpartgbij  31630  eulerpartlemn  31639  eulerpart  31640  ballotlemelo  31745  ballotleme  31754  ballotlem7  31793  reprsuc  31886  hgt750lema  31928  hgt750leme  31929  subfacp1lem6  32432  erdsze  32449  cvmscbv  32505  cvmsiota  32524  cvmlift2lem13  32562  satfv1  32610  neibastop2  33709  topdifinffin  34632  poimirlem27  34934  mblfinlem1  34944  mblfinlem2  34945  lclkrs2  38691  eldioph4i  39458  rfovcnvf1od  40399  fsovrfovd  40404  fsovcnvlem  40408  nzss  40698  supminfxr2  41794  limcperiod  41958  cncfshiftioo  42224  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvnprodlem1  42280  dvnprod  42283  itgiccshift  42314  itgperiod  42315  stoweidlem49  42383  fourierdlem41  42482  fourierdlem48  42488  fourierdlem49  42489  fourierdlem54  42494  fourierdlem65  42505  fourierdlem70  42510  fourierdlem71  42511  fourierdlem81  42521  fourierdlem89  42529  fourierdlem90  42530  fourierdlem91  42531  fourierdlem92  42532  fourierdlem96  42536  fourierdlem97  42537  fourierdlem98  42538  fourierdlem99  42539  fourierdlem100  42540  fourierdlem103  42543  fourierdlem104  42544  fourierdlem105  42545  fourierdlem108  42548  fourierdlem109  42549  fourierdlem110  42550  fourierdlem112  42552  fourierdlem113  42553  elaa2  42568  etransclem11  42579  etransc  42617  salexct  42666  subsaliuncl  42690  sge0fodjrnlem  42747  meadjiun  42797  ovnsubadd  42903  hoidmv1le  42925  hoidmvlelem3  42928  hoidmvlelem5  42930  ovnhoi  42934  hspmbllem3  42959  hspmbl  42960  opnvonmbl  42965  ovolval4lem2  42981  ovolval5lem2  42984  ovolval5lem3  42985  ovolval5  42986  ovnovol  42990  issmf  43054  incsmf  43068  issmfle  43071  issmfgt  43082  smfadd  43090  decsmf  43092  issmfge  43095  smflimlem4  43099  smflim  43102  smfmul  43119  smflimsuplem2  43144  smflimsuplem5  43147  smflimsuplem7  43149  requad2  43837