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  7361  oeeulem  8590  cofon1  8661  ordtypecbv  9490  ordtypelem9  9499  inf3lema  9604  oemapso  9662  oemapvali  9664  tz9.12lem3  9772  cofsmo  10272  enfin2i  10324  fin23lem33  10348  isf32lem11  10366  zorn2g  10506  pwfseqlem1  10668  pwfseqlem3  10670  zsupss  12987  zmin  12994  rpnnen1  13034  hashbc  14519  wrd2f1tovbij  15034  01sqrexlem7  15336  divalglem5  16488  bitsfzolem  16525  smupp1  16571  gcdcllem3  16592  bezout  16634  eulerth  16875  odzval  16884  pcprecl  16932  pcprendvds  16933  pcpremul  16936  pceulem  16938  prmreclem1  17009  prmreclem5  17013  prmreclem6  17014  4sqlem19  17056  vdwnn  17091  hashbcval  17095  gsumvalx  18779  symgfixelq  19561  efgsdm  19858  efgsfo  19867  ablfaclem3  20217  ltbwe  22261  coe1mul2lem2  22495  smadiadetlem3  22891  pptbas  23234  conncompss  23659  ptcmplem5  24283  ustuqtop  24473  utopsnneip  24475  icccmplem2  25051  minveclem5  25662  ivth  25683  ovolicc2lem5  25750  ovolicc  25752  opnmbllem  25830  vitali  25842  itg2monolem3  25981  elqaa  26555  radcnvle  26657  pserdvlem2  26665  lgamgulmlem5  27270  lgamcvglem  27277  wilth  27308  ftalem6  27315  precsexlemcbv  28472  bdayons  28542  ttgval  29332  axcontlem11  29432  lfgredgge2  29582  usgredgleordALT  29695  nbusgrf1o  29832  cusgrexg  29905  cusgrfilem2  29917  cusgrfi  29919  vtxdushgrfvedglem  29950  vtxdushgrfvedg  29951  vtxdginducedm1  30004  finsumvtxdg2sstep  30010  wwlksnextbij  30371  rusgrnumwwlks  30446  clwlkclwwlkfolem  30478  clwlkclwwlken  30483  clwwlknscsh  30533  hashecclwwlkn1  30548  umgrhashecclwwlk  30549  clwlknf1oclwwlknlem2  30553  clwlknf1oclwwlkn  30555  frgrwopreglem5lem  30801  frgrregorufr0  30805  fusgreghash2wsp  30819  dlwwlknondlwlknonf1o  30846  ubthlem3  31354  htth  31400  fcobijfs  33193  fcobijfs2  33194  elrgspnsubrunlem1  33688  elrgspnsubrun  33690  1arithufd  33959  extvfvcl  34047  mplvrpmfgalem  34055  constrsuc  34249  constrcbvlem  34266  locfinreflem  34351  zarmxt1  34391  zarcmp  34393  ordtconnlem1  34435  dynkin  34679  ddemeas  34748  oddpwdc  34866  eulerpartgbij  34884  eulerpartlemn  34893  eulerpart  34894  ballotlemelo  35000  ballotleme  35009  ballotlem7  35048  reprsuc  35124  hgt750lema  35166  hgt750leme  35167  fineqvnttrclse  35651  onvf1odlem3  35703  subfacp1lem6  35765  erdsze  35782  cvmscbv  35838  cvmsiota  35857  cvmlift2lem13  35895  satfv1  35943  neibastop2  36981  weiunfrlem  37084  topdifinffin  38103  poimirlem27  38397  mblfinlem1  38407  mblfinlem2  38408  lclkrs2  42414  aks4d1  42956  sticksstones2  43014  eldioph4i  43654  rfovcnvf1od  44845  fsovrfovd  44850  fsovcnvlem  44854  nzss  45142  supminfxr2  46298  limcperiod  46459  cncfshiftioo  46721  ioodvbdlimc1lem2  46761  ioodvbdlimc2lem  46763  dvnprodlem1  46775  dvnprod  46778  itgiccshift  46809  itgperiod  46810  stoweidlem49  46878  fourierdlem41  46977  fourierdlem48  46983  fourierdlem49  46984  fourierdlem54  46989  fourierdlem65  47000  fourierdlem70  47005  fourierdlem71  47006  fourierdlem81  47016  fourierdlem89  47024  fourierdlem90  47025  fourierdlem91  47026  fourierdlem92  47027  fourierdlem96  47031  fourierdlem97  47032  fourierdlem98  47033  fourierdlem99  47034  fourierdlem100  47035  fourierdlem103  47038  fourierdlem104  47039  fourierdlem105  47040  fourierdlem108  47043  fourierdlem109  47044  fourierdlem110  47045  fourierdlem112  47047  fourierdlem113  47048  elaa2  47063  etransclem11  47074  etransc  47112  salexct  47163  subsaliuncl  47187  sge0fodjrnlem  47245  meadjiun  47295  ovnsubadd  47401  hoidmv1le  47423  hoidmvlelem3  47426  hoidmvlelem5  47428  ovnhoi  47432  hspmbllem3  47457  hspmbl  47458  opnvonmbl  47463  ovolval4lem2  47479  ovolval5lem2  47482  ovolval5lem3  47483  ovolval5  47484  ovnovol  47488  issmf  47557  incsmf  47571  issmfle  47574  issmfgt  47585  smfadd  47594  decsmf  47596  issmfge  47599  smflimlem4  47603  smflim  47606  smfmul  47624  smflimsuplem2  47650  smflimsuplem5  47653  smflimsuplem7  47655  requad2  48540  uspgrlimlem1  48905  grlimedgclnbgr  48912  grlimgrtri  48920  gpgusgralem  48973  intubeu  49911  unilbeu  49912