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

Theorem cbvrabv 3105
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  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvrabv  |-  { x  e.  A  |  ph }  =  { y  e.  A  |  ps }
Distinct variable groups:    x, y, A    ph, y    ps, x
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem cbvrabv
StepHypRef Expression
1 nfcv 2616 . 2  |-  F/_ x A
2 nfcv 2616 . 2  |-  F/_ y A
3 nfv 1712 . 2  |-  F/ y
ph
4 nfv 1712 . 2  |-  F/ x ps
5 cbvrabv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
61, 2, 3, 4, 5cbvrab 3104 1  |-  { x  e.  A  |  ph }  =  { y  e.  A  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1398   {crab 2808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2813
This theorem is referenced by:  pwnss  4602  knatar  6228  oeeulem  7242  ordtypecbv  7934  ordtypelem9  7943  inf3lema  8032  oemapso  8092  oemapvali  8094  tz9.12lem3  8198  cofsmo  8640  enfin2i  8692  fin23lem33  8716  isf32lem11  8734  zorn2g  8874  pwfseqlem1  9025  pwfseqlem3  9027  zsupss  11172  zmin  11179  reexALT  11215  hashbc  12486  wrd2f1tovbij  12889  sqrlem7  13164  rpnnen  14044  divalglem5  14139  bitsfzolem  14168  smupp1  14214  gcdcllem3  14235  bezout  14264  eulerth  14397  odzval  14402  pcprecl  14447  pcprendvds  14448  pcpremul  14451  pceulem  14453  prmreclem1  14518  prmreclem5  14522  prmreclem6  14523  4sqlem19  14565  vdwnn  14600  hashbcval  14604  gsumvalx  16096  symgfixelq  16657  efgsdm  16947  efgsfo  16956  ablfaclem3  17333  ltbwe  18332  coe1mul2lem2  18504  smadiadetlem3  19337  pptbas  19676  concompss  20100  ptcmplem5  20722  ustuqtop  20915  utopsnneip  20917  icccmplem2  21494  minveclem5  22014  ivth  22032  ovolicc2lem5  22098  ovolicc  22100  opnmbllem  22176  vitali  22188  itg2monolem3  22325  elqaa  22884  radcnvle  22981  pserdvlem2  22989  wilth  23543  ftalem6  23549  ttgval  24380  axcontlem11  24479  nbgraf1olem1  24643  nbgraf1o  24649  cusgraexg  24671  cusgrafi  24684  wlknwwlknbij2  24916  wlkiswwlkbij2  24923  wwlkextbij  24935  wlknwwlknvbij  24942  clwwlkvbij  25003  clwwlknscsh  25021  hashecclwwlkn1  25036  usghashecclwwlk  25037  clwlksizeeq  25054  rusgranumwlklem4  25154  rusgranumwlks  25158  frgraregorufr0  25254  usgreghash2spot  25271  extwwlkfab  25292  numclwwlk5  25314  numclwwlk7  25316  ubthlem3  25986  htth  26033  fcobijfs  27780  locfinreflem  28078  ordtconlem1  28141  ddemeas  28445  oddpwdc  28557  eulerpartgbij  28575  eulerpartlemn  28584  eulerpart  28585  ballotlemelo  28690  ballotleme  28699  ballotlem7  28738  lgamgulmlem5  28839  lgamcvglem  28846  subfacp1lem6  28893  erdsze  28910  cvmscbv  28967  cvmsiota  28986  cvmlift2lem13  29024  mblfinlem1  30291  mblfinlem2  30292  neibastop2  30419  eldioph4i  30985  nzss  31463  limcperiod  31873  cncfshiftioo  31934  ioodvbdlimc1lem2  31968  ioodvbdlimc2lem  31970  dvnprodlem1  31982  dvnprod  31985  itgiccshift  32018  itgperiod  32019  stoweidlem49  32070  fourierdlem41  32169  fourierdlem48  32176  fourierdlem49  32177  fourierdlem54  32182  fourierdlem65  32193  fourierdlem70  32198  fourierdlem71  32199  fourierdlem81  32209  fourierdlem89  32217  fourierdlem90  32218  fourierdlem91  32219  fourierdlem92  32220  fourierdlem96  32224  fourierdlem97  32225  fourierdlem98  32226  fourierdlem99  32227  fourierdlem100  32228  fourierdlem103  32231  fourierdlem104  32232  fourierdlem105  32233  fourierdlem108  32236  fourierdlem109  32237  fourierdlem110  32238  fourierdlem112  32240  fourierdlem113  32241  elaa2  32256  etransclem11  32267  etransc  32305  usgedgleord  32791  usgedgleordALT  32792  lclkrs2  37664
  Copyright terms: Public domain W3C validator