Theorem cbvrabv 3396

Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. (Contributed by NM, 26-May-1999.)

Hypothesis

Ref	Expression
cbvrabv.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvrabv	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvrabv

Step	Hyp	Ref	Expression
1		nfcv 2955	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2955	. 2 ⊢ Ⅎ𝑦𝐴
3		nfv 2005	. 2 ⊢ Ⅎ𝑦𝜑
4		nfv 2005	. 2 ⊢ Ⅎ𝑥𝜓
5		cbvrabv.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvrab 3395	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1637  {crab 3107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-rab 3112

This theorem is referenced by:  rabrabi  3397  pwnss  5029  knatar  6834  oeeulem  7921  ordtypecbv  8664  ordtypelem9  8673  inf3lema  8771  oemapso  8829  oemapvali  8831  tz9.12lem3  8902  cofsmo  9379  enfin2i  9431  fin23lem33  9455  isf32lem11  9473  zorn2g  9613  pwfseqlem1  9768  pwfseqlem3  9770  zsupss  11999  zmin  12006  rpnnen1  12042  hashbc  13457  wrd2f1tovbij  13931  sqrlem7  14215  divalglem5  15343  bitsfzolem  15378  smupp1  15424  gcdcllem3  15445  bezout  15482  eulerth  15708  odzval  15716  pcprecl  15764  pcprendvds  15765  pcpremul  15768  pceulem  15770  prmreclem1  15840  prmreclem5  15844  prmreclem6  15845  4sqlem19  15887  vdwnn  15922  hashbcval  15926  gsumvalx  17478  symgfixelq  18057  efgsdm  18347  efgsfo  18356  ablfaclem3  18691  ltbwe  19684  coe1mul2lem2  19849  smadiadetlem3  20690  pptbas  21030  conncompss  21454  ptcmplem5  22077  ustuqtop  22267  utopsnneip  22269  icccmplem2  22843  minveclem5  23422  ivth  23441  ovolicc2lem5  23508  ovolicc  23510  opnmbllem  23588  vitali  23600  itg2monolem3  23739  elqaa  24297  radcnvle  24394  pserdvlem2  24402  lgamgulmlem5  24979  lgamcvglem  24986  wilth  25017  ftalem6  25024  ttgval  25975  axcontlem11  26074  lfgredgge2  26239  usgredgleordALT  26348  nbusgrf1o  26495  cusgrexg  26574  cusgrfilem2  26586  cusgrfi  26588  vtxdushgrfvedglem  26619  vtxdushgrfvedg  26620  vtxdginducedm1  26673  finsumvtxdg2sstep  26679  wlkwwlkbij2OLD  27033  wwlksnextbij  27045  wlksnwwlknvbijOLD  27052  rusgrnumwwlks  27122  clwlkclwwlkfolem  27156  clwlkclwwlken  27161  clwwlknscsh  27219  hashecclwwlkn1  27234  umgrhashecclwwlk  27235  clwlknf1oclwwlknlem2  27252  clwlknf1oclwwlkn  27254  clwlkssizeeqOLD  27256  clwwlkvbijOLD  27290  frgrwopreglem5lem  27501  frgrregorufr0  27505  fusgreghash2wsp  27519  dlwwlknondlwlknonf1o  27551  ubthlem3  28062  htth  28109  fcobijfs  29834  locfinreflem  30238  ordtconnlem1  30301  dynkin  30561  ddemeas  30630  oddpwdc  30747  eulerpartgbij  30765  eulerpartlemn  30774  eulerpart  30775  ballotlemelo  30880  ballotleme  30889  ballotlem7  30928  reprsuc  31024  hgt750lema  31066  hgt750leme  31067  subfacp1lem6  31495  erdsze  31512  cvmscbv  31568  cvmsiota  31587  cvmlift2lem13  31625  neibastop2  32682  topdifinffin  33514  poimirlem27  33751  mblfinlem1  33761  mblfinlem2  33762  lclkrs2  37322  eldioph4i  37879  rfovcnvf1od  38799  fsovrfovd  38804  fsovcnvlem  38808  nzss  39017  supminfxr2  40179  limcperiod  40341  cncfshiftioo  40586  ioodvbdlimc1lem2  40628  ioodvbdlimc2lem  40630  dvnprodlem1  40642  dvnprod  40645  itgiccshift  40676  itgperiod  40677  stoweidlem49  40746  fourierdlem41  40845  fourierdlem48  40851  fourierdlem49  40852  fourierdlem54  40857  fourierdlem65  40868  fourierdlem70  40873  fourierdlem71  40874  fourierdlem81  40884  fourierdlem89  40892  fourierdlem90  40893  fourierdlem91  40894  fourierdlem92  40895  fourierdlem96  40899  fourierdlem97  40900  fourierdlem98  40901  fourierdlem99  40902  fourierdlem100  40903  fourierdlem103  40906  fourierdlem104  40907  fourierdlem105  40908  fourierdlem108  40911  fourierdlem109  40912  fourierdlem110  40913  fourierdlem112  40915  fourierdlem113  40916  elaa2  40931  etransclem11  40942  etransc  40980  salexct  41032  subsaliuncl  41056  sge0fodjrnlem  41113  meadjiun  41163  ovnsubadd  41269  hoidmv1le  41291  hoidmvlelem3  41294  hoidmvlelem5  41296  ovnhoi  41300  hspmbllem3  41325  hspmbl  41326  opnvonmbl  41331  ovolval4lem2  41347  ovolval5lem2  41350  ovolval5lem3  41351  ovolval5  41352  ovnovol  41356  issmf  41420  incsmf  41434  issmfle  41437  issmfgt  41448  smfadd  41456  decsmf  41458  issmfge  41461  smflimlem4  41465  smflim  41468  smfmul  41485  smflimsuplem2  41510  smflimsuplem5  41513  smflimsuplem7  41515