MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvrabv Structured version   Visualization version   GIF version

Theorem cbvrabv 3171
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
StepHypRef Expression
1 nfcv 2750 . 2 𝑥𝐴
2 nfcv 2750 . 2 𝑦𝐴
3 nfv 1829 . 2 𝑦𝜑
4 nfv 1829 . 2 𝑥𝜓
5 cbvrabv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
61, 2, 3, 4, 5cbvrab 3170 1 {𝑥𝐴𝜑} = {𝑦𝐴𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  {crab 2899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904
This theorem is referenced by:  pwnss  4750  knatar  6484  oeeulem  7545  ordtypecbv  8282  ordtypelem9  8291  inf3lema  8381  oemapso  8439  oemapvali  8441  tz9.12lem3  8512  cofsmo  8951  enfin2i  9003  fin23lem33  9027  isf32lem11  9045  zorn2g  9185  pwfseqlem1  9336  pwfseqlem3  9338  zsupss  11611  zmin  11618  rpnnen1  11654  hashbc  13048  wrd2f1tovbij  13499  sqrlem7  13785  divalglem5  14906  bitsfzolem  14942  smupp1  14988  gcdcllem3  15009  bezout  15046  eulerth  15274  odzval  15282  pcprecl  15330  pcprendvds  15331  pcpremul  15334  pceulem  15336  prmreclem1  15406  prmreclem5  15410  prmreclem6  15411  4sqlem19  15453  vdwnn  15488  hashbcval  15492  gsumvalx  17041  symgfixelq  17624  efgsdm  17914  efgsfo  17923  ablfaclem3  18257  ltbwe  19241  coe1mul2lem2  19407  smadiadetlem3  20240  pptbas  20569  concompss  20993  ptcmplem5  21617  ustuqtop  21807  utopsnneip  21809  icccmplem2  22381  minveclem5  22956  ivth  22974  ovolicc2lem5  23040  ovolicc  23042  opnmbllem  23119  vitali  23132  itg2monolem3  23269  elqaa  23825  radcnvle  23922  pserdvlem2  23930  lgamgulmlem5  24503  lgamcvglem  24510  wilth  24541  ftalem6  24548  ttgval  25500  axcontlem11  25599  nbgraf1olem1  25763  nbgraf1o  25769  cusgraexg  25791  cusgrafi  25803  wlknwwlknbij2  26035  wlkiswwlkbij2  26042  wwlkextbij  26054  wlknwwlknvbij  26061  clwwlkvbij  26122  clwwlknscsh  26140  hashecclwwlkn1  26154  usghashecclwwlk  26155  clwlksizeeq  26172  rusgranumwlklem4  26272  rusgranumwlks  26276  frgraregorufr0  26372  usgreghash2spot  26389  extwwlkfab  26410  numclwwlk5  26432  numclwwlk7  26434  ubthlem3  26905  htth  26952  fcobijfs  28682  locfinreflem  29028  ordtconlem1  29091  dynkin  29350  ddemeas  29419  oddpwdc  29536  eulerpartgbij  29554  eulerpartlemn  29563  eulerpart  29564  ballotlemelo  29669  ballotleme  29678  ballotlem7  29717  subfacp1lem6  30214  erdsze  30231  cvmscbv  30287  cvmsiota  30306  cvmlift2lem13  30344  neibastop2  31319  topdifinffin  32155  poimirlem27  32389  mblfinlem1  32399  mblfinlem2  32400  lclkrs2  35630  eldioph4i  36177  rfovcnvf1od  37101  fsovrfovd  37106  fsovcnvlem  37110  nzss  37321  limcperiod  38478  cncfshiftioo  38561  ioodvbdlimc1lem2  38605  ioodvbdlimc2lem  38607  dvnprodlem1  38619  dvnprod  38622  itgiccshift  38655  itgperiod  38656  stoweidlem49  38725  fourierdlem41  38824  fourierdlem48  38830  fourierdlem49  38831  fourierdlem54  38836  fourierdlem65  38847  fourierdlem70  38852  fourierdlem71  38853  fourierdlem81  38863  fourierdlem89  38871  fourierdlem90  38872  fourierdlem91  38873  fourierdlem92  38874  fourierdlem96  38878  fourierdlem97  38879  fourierdlem98  38880  fourierdlem99  38881  fourierdlem100  38882  fourierdlem103  38885  fourierdlem104  38886  fourierdlem105  38887  fourierdlem108  38890  fourierdlem109  38891  fourierdlem110  38892  fourierdlem112  38894  fourierdlem113  38895  elaa2  38910  etransclem11  38921  etransc  38959  salexct  39011  subsaliuncl  39035  sge0fodjrnlem  39092  meadjiun  39142  ovnsubadd  39245  hoidmv1le  39267  hoidmvlelem3  39270  hoidmvlelem5  39272  ovnhoi  39276  hspmbllem3  39301  hspmbl  39302  opnvonmbl  39307  ovolval4lem2  39323  ovolval5lem2  39326  ovolval5lem3  39327  ovolval5  39328  ovnovol  39332  issmf  39397  incsmf  39412  issmfle  39415  issmfgt  39426  smfadd  39434  decsmf  39436  issmfge  39439  smflimlem4  39443  smflim  39446  smfmul  39463  lfgredgge2  40330  usgredgaleordALT  40442  nbusgrf1o  40580  cusgrexg  40644  cusgrfilem2  40653  cusgrfi  40655  vtxdushgrfvedglem  40685  vtxdushgrfvedg  40686  wlknwwlksnbij2  41070  wlkwwlkbij2  41077  wwlksnextbij  41089  wlksnwwlknvbij  41095  rusgrnumwwlks  41158  clwwlksvbij  41210  clwwlksnscsh  41228  hashecclwwlksn1  41242  umgrhashecclwwlk  41243  clwlkssizeeq  41259  frgrregorufr0  41470  fusgreghash2wsp  41483  av-extwwlkfab  41501  av-numclwwlk5  41523  av-numclwwlk6  41525
  Copyright terms: Public domain W3C validator