Theorem cbvrabv 3443

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 2154 and ax-13 2374. (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 2821	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2809	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3433	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3433	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2772	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536   ∈ wcel 2105  {cab 2711  {crab 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433

This theorem is referenced by:  rabrabiOLD  3458  rru  3787  knatar  7376  oeeulem  8637  cofon1  8708  ordtypecbv  9554  ordtypelem9  9563  inf3lema  9661  oemapso  9719  oemapvali  9721  tz9.12lem3  9826  cofsmo  10306  enfin2i  10358  fin23lem33  10382  isf32lem11  10400  zorn2g  10540  pwfseqlem1  10695  pwfseqlem3  10697  zsupss  12976  zmin  12983  rpnnen1  13022  hashbc  14488  wrd2f1tovbij  14995  01sqrexlem7  15283  divalglem5  16430  bitsfzolem  16467  smupp1  16513  gcdcllem3  16534  bezout  16576  eulerth  16816  odzval  16824  pcprecl  16872  pcprendvds  16873  pcpremul  16876  pceulem  16878  prmreclem1  16949  prmreclem5  16953  prmreclem6  16954  4sqlem19  16996  vdwnn  17031  hashbcval  17035  gsumvalx  18701  symgfixelq  19465  efgsdm  19762  efgsfo  19771  ablfaclem3  20121  ltbwe  22079  coe1mul2lem2  22286  smadiadetlem3  22689  pptbas  23030  conncompss  23456  ptcmplem5  24079  ustuqtop  24270  utopsnneip  24272  icccmplem2  24858  minveclem5  25480  ivth  25502  ovolicc2lem5  25569  ovolicc  25571  opnmbllem  25649  vitali  25661  itg2monolem3  25801  elqaa  26378  radcnvle  26477  pserdvlem2  26486  lgamgulmlem5  27090  lgamcvglem  27097  wilth  27128  ftalem6  27135  precsexlemcbv  28244  ttgval  28897  ttgvalOLD  28898  axcontlem11  29003  lfgredgge2  29155  usgredgleordALT  29265  nbusgrf1o  29402  cusgrexg  29475  cusgrfilem2  29488  cusgrfi  29490  vtxdushgrfvedglem  29521  vtxdushgrfvedg  29522  vtxdginducedm1  29575  finsumvtxdg2sstep  29581  wwlksnextbij  29931  rusgrnumwwlks  30003  clwlkclwwlkfolem  30035  clwlkclwwlken  30040  clwwlknscsh  30090  hashecclwwlkn1  30105  umgrhashecclwwlk  30106  clwlknf1oclwwlknlem2  30110  clwlknf1oclwwlkn  30112  frgrwopreglem5lem  30348  frgrregorufr0  30352  fusgreghash2wsp  30366  dlwwlknondlwlknonf1o  30393  ubthlem3  30900  htth  30946  fcobijfs  32740  1arithufd  33555  constrsuc  33742  locfinreflem  33800  zarmxt1  33840  zarcmp  33842  ordtconnlem1  33884  dynkin  34147  ddemeas  34216  oddpwdc  34335  eulerpartgbij  34353  eulerpartlemn  34362  eulerpart  34363  ballotlemelo  34468  ballotleme  34477  ballotlem7  34516  reprsuc  34608  hgt750lema  34650  hgt750leme  34651  subfacp1lem6  35169  erdsze  35186  cvmscbv  35242  cvmsiota  35261  cvmlift2lem13  35299  satfv1  35347  neibastop2  36343  weiunfrlem  36446  topdifinffin  37330  poimirlem27  37633  mblfinlem1  37643  mblfinlem2  37644  lclkrs2  41522  aks4d1  42070  sticksstones2  42128  eldioph4i  42799  rfovcnvf1od  43993  fsovrfovd  43998  fsovcnvlem  44002  nzss  44312  supminfxr2  45418  limcperiod  45583  cncfshiftioo  45847  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnprodlem1  45901  dvnprod  45904  itgiccshift  45935  itgperiod  45936  stoweidlem49  46004  fourierdlem41  46103  fourierdlem48  46109  fourierdlem49  46110  fourierdlem54  46115  fourierdlem65  46126  fourierdlem70  46131  fourierdlem71  46132  fourierdlem81  46142  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem92  46153  fourierdlem96  46157  fourierdlem97  46158  fourierdlem98  46159  fourierdlem99  46160  fourierdlem100  46161  fourierdlem103  46164  fourierdlem104  46165  fourierdlem105  46166  fourierdlem108  46169  fourierdlem109  46170  fourierdlem110  46171  fourierdlem112  46173  fourierdlem113  46174  elaa2  46189  etransclem11  46200  etransc  46238  salexct  46289  subsaliuncl  46313  sge0fodjrnlem  46371  meadjiun  46421  ovnsubadd  46527  hoidmv1le  46549  hoidmvlelem3  46552  hoidmvlelem5  46554  ovnhoi  46558  hspmbllem3  46583  hspmbl  46584  opnvonmbl  46589  ovolval4lem2  46605  ovolval5lem2  46608  ovolval5lem3  46609  ovolval5  46610  ovnovol  46614  issmf  46683  incsmf  46697  issmfle  46700  issmfgt  46711  smfadd  46720  decsmf  46722  issmfge  46725  smflimlem4  46729  smflim  46732  smfmul  46750  smflimsuplem2  46776  smflimsuplem5  46779  smflimsuplem7  46781  requad2  47547  uspgrlimlem1  47890  grlimgrtri  47898  gpgusgralem  47945  intubeu  48772  unilbeu  48773