Theorem cbvrabv 3172

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 2751	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2751	. 2 ⊢ Ⅎ𝑦𝐴
3		nfv 1830	. 2 ⊢ Ⅎ𝑦𝜑
4		nfv 1830	. 2 ⊢ Ⅎ𝑥𝜓
5		cbvrabv.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
6	1, 2, 3, 4, 5	cbvrab 3171	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  {crab 2900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905

This theorem is referenced by:  pwnss  4756  knatar  6507  oeeulem  7568  ordtypecbv  8305  ordtypelem9  8314  inf3lema  8404  oemapso  8462  oemapvali  8464  tz9.12lem3  8535  cofsmo  8974  enfin2i  9026  fin23lem33  9050  isf32lem11  9068  zorn2g  9208  pwfseqlem1  9359  pwfseqlem3  9361  zsupss  11653  zmin  11660  rpnnen1  11696  hashbc  13094  wrd2f1tovbij  13551  sqrlem7  13837  divalglem5  14958  bitsfzolem  14994  smupp1  15040  gcdcllem3  15061  bezout  15098  eulerth  15326  odzval  15334  pcprecl  15382  pcprendvds  15383  pcpremul  15386  pceulem  15388  prmreclem1  15458  prmreclem5  15462  prmreclem6  15463  4sqlem19  15505  vdwnn  15540  hashbcval  15544  gsumvalx  17093  symgfixelq  17676  efgsdm  17966  efgsfo  17975  ablfaclem3  18309  ltbwe  19293  coe1mul2lem2  19459  smadiadetlem3  20293  pptbas  20622  concompss  21046  ptcmplem5  21670  ustuqtop  21860  utopsnneip  21862  icccmplem2  22434  minveclem5  23012  ivth  23030  ovolicc2lem5  23096  ovolicc  23098  opnmbllem  23175  vitali  23188  itg2monolem3  23325  elqaa  23881  radcnvle  23978  pserdvlem2  23986  lgamgulmlem5  24559  lgamcvglem  24566  wilth  24597  ftalem6  24604  ttgval  25555  axcontlem11  25654  lfgredgge2  25790  nbgraf1olem1  25970  nbgraf1o  25976  cusgraexg  25998  cusgrafi  26010  wlknwwlknbij2  26242  wlkiswwlkbij2  26249  wwlkextbij  26261  wlknwwlknvbij  26268  clwwlkvbij  26329  clwwlknscsh  26347  hashecclwwlkn1  26361  usghashecclwwlk  26362  clwlksizeeq  26379  rusgranumwlklem4  26479  rusgranumwlks  26483  frgraregorufr0  26579  usgreghash2spot  26596  extwwlkfab  26617  numclwwlk5  26639  numclwwlk7  26641  ubthlem3  27112  htth  27159  fcobijfs  28889  locfinreflem  29235  ordtconlem1  29298  dynkin  29557  ddemeas  29626  oddpwdc  29743  eulerpartgbij  29761  eulerpartlemn  29770  eulerpart  29771  ballotlemelo  29876  ballotleme  29885  ballotlem7  29924  subfacp1lem6  30421  erdsze  30438  cvmscbv  30494  cvmsiota  30513  cvmlift2lem13  30551  neibastop2  31526  topdifinffin  32372  poimirlem27  32606  mblfinlem1  32616  mblfinlem2  32617  lclkrs2  35847  eldioph4i  36394  rfovcnvf1od  37318  fsovrfovd  37323  fsovcnvlem  37327  nzss  37538  limcperiod  38695  cncfshiftioo  38778  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnprodlem1  38836  dvnprod  38839  itgiccshift  38872  itgperiod  38873  stoweidlem49  38942  fourierdlem41  39041  fourierdlem48  39047  fourierdlem49  39048  fourierdlem54  39053  fourierdlem65  39064  fourierdlem70  39069  fourierdlem71  39070  fourierdlem81  39080  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem92  39091  fourierdlem96  39095  fourierdlem97  39096  fourierdlem98  39097  fourierdlem99  39098  fourierdlem100  39099  fourierdlem103  39102  fourierdlem104  39103  fourierdlem105  39104  fourierdlem108  39107  fourierdlem109  39108  fourierdlem110  39109  fourierdlem112  39111  fourierdlem113  39112  elaa2  39127  etransclem11  39138  etransc  39176  salexct  39228  subsaliuncl  39252  sge0fodjrnlem  39309  meadjiun  39359  ovnsubadd  39462  hoidmv1le  39484  hoidmvlelem3  39487  hoidmvlelem5  39489  ovnhoi  39493  hspmbllem3  39518  hspmbl  39519  opnvonmbl  39524  ovolval4lem2  39540  ovolval5lem2  39543  ovolval5lem3  39544  ovolval5  39545  ovnovol  39549  issmf  39614  incsmf  39629  issmfle  39632  issmfgt  39643  smfadd  39651  decsmf  39653  issmfge  39656  smflimlem4  39660  smflim  39663  smfmul  39680  usgredgaleordALT  40461  nbusgrf1o  40599  cusgrexg  40663  cusgrfilem2  40672  cusgrfi  40674  vtxdushgrfvedglem  40704  vtxdushgrfvedg  40705  wlknwwlksnbij2  41089  wlkwwlkbij2  41096  wwlksnextbij  41108  wlksnwwlknvbij  41114  rusgrnumwwlks  41177  clwwlksvbij  41229  clwwlksnscsh  41247  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  clwlkssizeeq  41278  frgrregorufr0  41489  fusgreghash2wsp  41502  av-extwwlkfab  41520  av-numclwwlk5  41542  av-numclwwlk6  41544