Theorem cbvrabv 3426

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 2192 and ax-13 2404. (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 2846	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 643	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2833	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3417	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3417	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2796	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  {cab 2741  {crab 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417

This theorem is referenced by:  rru  3743  knatar  7357  oeeulem  8588  cofon1  8659  ordtypecbv  9480  ordtypelem9  9489  inf3lema  9594  oemapso  9652  oemapvali  9654  tz9.12lem3  9762  cofsmo  10254  enfin2i  10306  fin23lem33  10330  isf32lem11  10348  zorn2g  10488  pwfseqlem1  10644  pwfseqlem3  10646  zsupss  12962  zmin  12969  rpnnen1  13008  hashbc  14492  wrd2f1tovbij  14999  01sqrexlem7  15301  divalglem5  16456  bitsfzolem  16493  smupp1  16539  gcdcllem3  16560  bezout  16602  eulerth  16843  odzval  16852  pcprecl  16900  pcprendvds  16901  pcpremul  16904  pceulem  16906  prmreclem1  16977  prmreclem5  16981  prmreclem6  16982  4sqlem19  17024  vdwnn  17059  hashbcval  17063  gsumvalx  18735  symgfixelq  19504  efgsdm  19801  efgsfo  19810  ablfaclem3  20160  ltbwe  22176  coe1mul2lem2  22410  smadiadetlem3  22806  pptbas  23146  conncompss  23571  ptcmplem5  24194  ustuqtop  24384  utopsnneip  24386  icccmplem2  24962  minveclem5  25573  ivth  25594  ovolicc2lem5  25661  ovolicc  25663  opnmbllem  25741  vitali  25753  itg2monolem3  25892  elqaa  26464  radcnvle  26564  pserdvlem2  26572  lgamgulmlem5  27178  lgamcvglem  27185  wilth  27216  ftalem6  27223  precsexlemcbv  28380  bdayons  28450  ttgval  29205  axcontlem11  29305  lfgredgge2  29455  usgredgleordALT  29565  nbusgrf1o  29702  cusgrexg  29775  cusgrfilem2  29787  cusgrfi  29789  vtxdushgrfvedglem  29820  vtxdushgrfvedg  29821  vtxdginducedm1  29874  finsumvtxdg2sstep  29880  wwlksnextbij  30232  rusgrnumwwlks  30307  clwlkclwwlkfolem  30339  clwlkclwwlken  30344  clwwlknscsh  30394  hashecclwwlkn1  30409  umgrhashecclwwlk  30410  clwlknf1oclwwlknlem2  30414  clwlknf1oclwwlkn  30416  frgrwopreglem5lem  30652  frgrregorufr0  30656  fusgreghash2wsp  30670  dlwwlknondlwlknonf1o  30697  ubthlem3  31205  htth  31251  fcobijfs  33047  fcobijfs2  33048  elrgspnsubrunlem1  33548  elrgspnsubrun  33550  1arithufd  33819  extvfvcl  33907  mplvrpmfgalem  33915  constrsuc  34109  constrcbvlem  34126  locfinreflem  34211  zarmxt1  34251  zarcmp  34253  ordtconnlem1  34295  dynkin  34538  ddemeas  34607  oddpwdc  34725  eulerpartgbij  34743  eulerpartlemn  34752  eulerpart  34753  ballotlemelo  34859  ballotleme  34868  ballotlem7  34907  reprsuc  34983  hgt750lema  35025  hgt750leme  35026  fineqvnttrclse  35518  onvf1odlem3  35570  subfacp1lem6  35658  erdsze  35675  cvmscbv  35731  cvmsiota  35750  cvmlift2lem13  35788  satfv1  35836  neibastop2  36853  weiunfrlem  36956  topdifinffin  37975  poimirlem27  38279  mblfinlem1  38289  mblfinlem2  38290  lclkrs2  42295  aks4d1  42837  sticksstones2  42895  eldioph4i  43522  rfovcnvf1od  44713  fsovrfovd  44718  fsovcnvlem  44722  nzss  45010  supminfxr2  46166  limcperiod  46327  cncfshiftioo  46589  ioodvbdlimc1lem2  46629  ioodvbdlimc2lem  46631  dvnprodlem1  46643  dvnprod  46646  itgiccshift  46677  itgperiod  46678  stoweidlem49  46746  fourierdlem41  46845  fourierdlem48  46851  fourierdlem49  46852  fourierdlem54  46857  fourierdlem65  46868  fourierdlem70  46873  fourierdlem71  46874  fourierdlem81  46884  fourierdlem89  46892  fourierdlem90  46893  fourierdlem91  46894  fourierdlem92  46895  fourierdlem96  46899  fourierdlem97  46900  fourierdlem98  46901  fourierdlem99  46902  fourierdlem100  46903  fourierdlem103  46906  fourierdlem104  46907  fourierdlem105  46908  fourierdlem108  46911  fourierdlem109  46912  fourierdlem110  46913  fourierdlem112  46915  fourierdlem113  46916  elaa2  46931  etransclem11  46942  etransc  46980  salexct  47031  subsaliuncl  47055  sge0fodjrnlem  47113  meadjiun  47163  ovnsubadd  47269  hoidmv1le  47291  hoidmvlelem3  47294  hoidmvlelem5  47296  ovnhoi  47300  hspmbllem3  47325  hspmbl  47326  opnvonmbl  47331  ovolval4lem2  47347  ovolval5lem2  47350  ovolval5lem3  47351  ovolval5  47352  ovnovol  47356  issmf  47425  incsmf  47439  issmfle  47442  issmfgt  47453  smfadd  47462  decsmf  47464  issmfge  47467  smflimlem4  47471  smflim  47474  smfmul  47492  smflimsuplem2  47518  smflimsuplem5  47521  smflimsuplem7  47523  requad2  48371  uspgrlimlem1  48736  grlimedgclnbgr  48743  grlimgrtri  48751  gpgusgralem  48804  intubeu  49745  unilbeu  49746