Theorem cbvrabv 3402

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 2371. (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 2820	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 634	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2811	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3070	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3070	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2775	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543   ∈ wcel 2110  {cab 2714  {crab 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070

This theorem is referenced by:  rabrabiOLD  3404  rru  3692  knatar  7166  oeeulem  8329  ordtypecbv  9133  ordtypelem9  9142  inf3lema  9239  oemapso  9297  oemapvali  9299  tz9.12lem3  9405  cofsmo  9883  enfin2i  9935  fin23lem33  9959  isf32lem11  9977  zorn2g  10117  pwfseqlem1  10272  pwfseqlem3  10274  zsupss  12533  zmin  12540  rpnnen1  12579  hashbc  14017  wrd2f1tovbij  14527  sqrlem7  14812  divalglem5  15958  bitsfzolem  15993  smupp1  16039  gcdcllem3  16060  bezout  16103  eulerth  16336  odzval  16344  pcprecl  16392  pcprendvds  16393  pcpremul  16396  pceulem  16398  prmreclem1  16469  prmreclem5  16473  prmreclem6  16474  4sqlem19  16516  vdwnn  16551  hashbcval  16555  gsumvalx  18148  symgfixelq  18825  efgsdm  19120  efgsfo  19129  ablfaclem3  19474  ltbwe  21001  coe1mul2lem2  21189  smadiadetlem3  21565  pptbas  21905  conncompss  22330  ptcmplem5  22953  ustuqtop  23144  utopsnneip  23146  icccmplem2  23720  minveclem5  24330  ivth  24351  ovolicc2lem5  24418  ovolicc  24420  opnmbllem  24498  vitali  24510  itg2monolem3  24650  elqaa  25215  radcnvle  25312  pserdvlem2  25320  lgamgulmlem5  25915  lgamcvglem  25922  wilth  25953  ftalem6  25960  ttgval  26966  axcontlem11  27065  lfgredgge2  27215  usgredgleordALT  27322  nbusgrf1o  27459  cusgrexg  27532  cusgrfilem2  27544  cusgrfi  27546  vtxdushgrfvedglem  27577  vtxdushgrfvedg  27578  vtxdginducedm1  27631  finsumvtxdg2sstep  27637  wwlksnextbij  27986  rusgrnumwwlks  28058  clwlkclwwlkfolem  28090  clwlkclwwlken  28095  clwwlknscsh  28145  hashecclwwlkn1  28160  umgrhashecclwwlk  28161  clwlknf1oclwwlknlem2  28165  clwlknf1oclwwlkn  28167  frgrwopreglem5lem  28403  frgrregorufr0  28407  fusgreghash2wsp  28421  dlwwlknondlwlknonf1o  28448  ubthlem3  28953  htth  28999  fcobijfs  30778  locfinreflem  31504  zarmxt1  31544  zarcmp  31546  ordtconnlem1  31588  dynkin  31847  ddemeas  31916  oddpwdc  32033  eulerpartgbij  32051  eulerpartlemn  32060  eulerpart  32061  ballotlemelo  32166  ballotleme  32175  ballotlem7  32214  reprsuc  32307  hgt750lema  32349  hgt750leme  32350  subfacp1lem6  32860  erdsze  32877  cvmscbv  32933  cvmsiota  32952  cvmlift2lem13  32990  satfv1  33038  neibastop2  34287  topdifinffin  35256  poimirlem27  35541  mblfinlem1  35551  mblfinlem2  35552  lclkrs2  39291  sticksstones2  39825  eldioph4i  40337  rfovcnvf1od  41289  fsovrfovd  41294  fsovcnvlem  41298  nzss  41608  supminfxr2  42684  limcperiod  42844  cncfshiftioo  43108  ioodvbdlimc1lem2  43148  ioodvbdlimc2lem  43150  dvnprodlem1  43162  dvnprod  43165  itgiccshift  43196  itgperiod  43197  stoweidlem49  43265  fourierdlem41  43364  fourierdlem48  43370  fourierdlem49  43371  fourierdlem54  43376  fourierdlem65  43387  fourierdlem70  43392  fourierdlem71  43393  fourierdlem81  43403  fourierdlem89  43411  fourierdlem90  43412  fourierdlem91  43413  fourierdlem92  43414  fourierdlem96  43418  fourierdlem97  43419  fourierdlem98  43420  fourierdlem99  43421  fourierdlem100  43422  fourierdlem103  43425  fourierdlem104  43426  fourierdlem105  43427  fourierdlem108  43430  fourierdlem109  43431  fourierdlem110  43432  fourierdlem112  43434  fourierdlem113  43435  elaa2  43450  etransclem11  43461  etransc  43499  salexct  43548  subsaliuncl  43572  sge0fodjrnlem  43629  meadjiun  43679  ovnsubadd  43785  hoidmv1le  43807  hoidmvlelem3  43810  hoidmvlelem5  43812  ovnhoi  43816  hspmbllem3  43841  hspmbl  43842  opnvonmbl  43847  ovolval4lem2  43863  ovolval5lem2  43866  ovolval5lem3  43867  ovolval5  43868  ovnovol  43872  issmf  43936  incsmf  43950  issmfle  43953  issmfgt  43964  smfadd  43972  decsmf  43974  issmfge  43977  smflimlem4  43981  smflim  43984  smfmul  44001  smflimsuplem2  44026  smflimsuplem5  44029  smflimsuplem7  44031  requad2  44748  intubeu  45943  unilbeu  45944