Theorem cbvrabv 3416

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 2158 and ax-13 2370. (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 2811	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2799	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3406	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3406	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2762	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {cab 2707  {crab 3405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406

This theorem is referenced by:  rru  3750  knatar  7332  oeeulem  8565  cofon1  8636  ordtypecbv  9470  ordtypelem9  9479  inf3lema  9577  oemapso  9635  oemapvali  9637  tz9.12lem3  9742  cofsmo  10222  enfin2i  10274  fin23lem33  10298  isf32lem11  10316  zorn2g  10456  pwfseqlem1  10611  pwfseqlem3  10613  zsupss  12896  zmin  12903  rpnnen1  12942  hashbc  14418  wrd2f1tovbij  14926  01sqrexlem7  15214  divalglem5  16367  bitsfzolem  16404  smupp1  16450  gcdcllem3  16471  bezout  16513  eulerth  16753  odzval  16762  pcprecl  16810  pcprendvds  16811  pcpremul  16814  pceulem  16816  prmreclem1  16887  prmreclem5  16891  prmreclem6  16892  4sqlem19  16934  vdwnn  16969  hashbcval  16973  gsumvalx  18603  symgfixelq  19363  efgsdm  19660  efgsfo  19669  ablfaclem3  20019  ltbwe  21951  coe1mul2lem2  22154  smadiadetlem3  22555  pptbas  22895  conncompss  23320  ptcmplem5  23943  ustuqtop  24134  utopsnneip  24136  icccmplem2  24712  minveclem5  25333  ivth  25355  ovolicc2lem5  25422  ovolicc  25424  opnmbllem  25502  vitali  25514  itg2monolem3  25653  elqaa  26230  radcnvle  26329  pserdvlem2  26338  lgamgulmlem5  26943  lgamcvglem  26950  wilth  26981  ftalem6  26988  precsexlemcbv  28108  bdayon  28173  ttgval  28802  axcontlem11  28901  lfgredgge2  29051  usgredgleordALT  29161  nbusgrf1o  29298  cusgrexg  29371  cusgrfilem2  29384  cusgrfi  29386  vtxdushgrfvedglem  29417  vtxdushgrfvedg  29418  vtxdginducedm1  29471  finsumvtxdg2sstep  29477  wwlksnextbij  29832  rusgrnumwwlks  29904  clwlkclwwlkfolem  29936  clwlkclwwlken  29941  clwwlknscsh  29991  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  clwlknf1oclwwlknlem2  30011  clwlknf1oclwwlkn  30013  frgrwopreglem5lem  30249  frgrregorufr0  30253  fusgreghash2wsp  30267  dlwwlknondlwlknonf1o  30294  ubthlem3  30801  htth  30847  fcobijfs  32646  elrgspnsubrunlem1  33198  elrgspnsubrun  33200  1arithufd  33519  constrsuc  33728  constrcbvlem  33745  locfinreflem  33830  zarmxt1  33870  zarcmp  33872  ordtconnlem1  33914  dynkin  34157  ddemeas  34226  oddpwdc  34345  eulerpartgbij  34363  eulerpartlemn  34372  eulerpart  34373  ballotlemelo  34479  ballotleme  34488  ballotlem7  34527  reprsuc  34606  hgt750lema  34648  hgt750leme  34649  onvf1odlem3  35092  subfacp1lem6  35172  erdsze  35189  cvmscbv  35245  cvmsiota  35264  cvmlift2lem13  35302  satfv1  35350  neibastop2  36349  weiunfrlem  36452  topdifinffin  37336  poimirlem27  37641  mblfinlem1  37651  mblfinlem2  37652  lclkrs2  41534  aks4d1  42077  sticksstones2  42135  eldioph4i  42800  rfovcnvf1od  43993  fsovrfovd  43998  fsovcnvlem  44002  nzss  44306  supminfxr2  45465  limcperiod  45626  cncfshiftioo  45890  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnprodlem1  45944  dvnprod  45947  itgiccshift  45978  itgperiod  45979  stoweidlem49  46047  fourierdlem41  46146  fourierdlem48  46152  fourierdlem49  46153  fourierdlem54  46158  fourierdlem65  46169  fourierdlem70  46174  fourierdlem71  46175  fourierdlem81  46185  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem92  46196  fourierdlem96  46200  fourierdlem97  46201  fourierdlem98  46202  fourierdlem99  46203  fourierdlem100  46204  fourierdlem103  46207  fourierdlem104  46208  fourierdlem105  46209  fourierdlem108  46212  fourierdlem109  46213  fourierdlem110  46214  fourierdlem112  46216  fourierdlem113  46217  elaa2  46232  etransclem11  46243  etransc  46281  salexct  46332  subsaliuncl  46356  sge0fodjrnlem  46414  meadjiun  46464  ovnsubadd  46570  hoidmv1le  46592  hoidmvlelem3  46595  hoidmvlelem5  46597  ovnhoi  46601  hspmbllem3  46626  hspmbl  46627  opnvonmbl  46632  ovolval4lem2  46648  ovolval5lem2  46651  ovolval5lem3  46652  ovolval5  46653  ovnovol  46657  issmf  46726  incsmf  46740  issmfle  46743  issmfgt  46754  smfadd  46763  decsmf  46765  issmfge  46768  smflimlem4  46772  smflim  46775  smfmul  46793  smflimsuplem2  46819  smflimsuplem5  46822  smflimsuplem7  46824  requad2  47624  uspgrlimlem1  47987  grlimgrtri  47995  gpgusgralem  48047  intubeu  48972  unilbeu  48973