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

Theorem cbvrabv 2976
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 2584 . 2  |-  F/_ x A
2 nfcv 2584 . 2  |-  F/_ y A
3 nfv 1673 . 2  |-  F/ y
ph
4 nfv 1673 . 2  |-  F/ x ps
5 cbvrabv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
61, 2, 3, 4, 5cbvrab 2975 1  |-  { x  e.  A  |  ph }  =  { y  e.  A  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369   {crab 2724
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-rab 2729
This theorem is referenced by:  pwnss  4462  knatar  6053  oeeulem  7045  ordtypecbv  7736  ordtypelem9  7745  inf3lema  7835  oemapso  7895  oemapvali  7897  tz9.12lem3  8001  cofsmo  8443  enfin2i  8495  fin23lem33  8519  isf32lem11  8537  zorn2g  8677  pwfseqlem1  8830  pwfseqlem3  8832  zsupss  10949  zmin  10954  reexALT  10990  hashbc  12211  sqrlem7  12743  rpnnen  13514  divalglem5  13606  bitsfzolem  13635  smupp1  13681  gcdcllem3  13702  bezout  13731  eulerth  13863  odzval  13868  pcprecl  13911  pcprendvds  13912  pcpremul  13915  pceulem  13917  prmreclem1  13982  prmreclem5  13986  prmreclem6  13987  4sqlem19  14029  vdwnn  14064  hashbcval  14068  gsumvalx  15507  symgfixelq  15943  efgsdm  16232  efgsfo  16241  ablfaclem3  16593  ltbwe  17559  coe1mul2lem2  17727  smadiadetlem3  18479  pptbas  18617  concompss  19042  ptcmplem5  19633  ustuqtop  19826  utopsnneip  19828  icccmplem2  20405  minveclem5  20925  ivth  20943  ovolicc2lem5  21009  ovolicc  21011  opnmbllem  21086  vitali  21098  itg2monolem3  21235  elqaa  21793  radcnvle  21890  pserdvlem2  21898  wilth  22414  ftalem6  22420  ttgval  23126  axcontlem11  23225  nbgraf1olem1  23355  nbgraf1o  23361  cusgraexg  23382  cusgrafi  23395  ubthlem3  24278  htth  24325  ordtconlem1  26359  ddemeas  26657  oddpwdc  26742  eulerpartgbij  26760  eulerpartlemn  26769  eulerpart  26770  ballotlemelo  26875  ballotleme  26884  ballotlem7  26923  lgamgulmlem5  27024  lgamcvglem  27031  subfacp1lem6  27078  erdsze  27095  cvmscbv  27152  cvmsiota  27171  cvmlift2lem13  27209  mblfinlem1  28433  mblfinlem2  28434  neibastop2  28587  eldioph4i  29156  stoweidlem49  29849  wrd2f1tovbij  30260  wlknwwlknbij2  30351  wlkiswwlkbij2  30358  wwlkextbij  30370  wlknwwlknvbij  30377  clwwlkvbij  30468  Lemma2  30498  hashecclwwlkn1  30513  usghashecclwwlk  30514  clwlksizeeq  30530  rusgranumwlklem4  30575  rusgranumwlks  30579  frgraregorufr0  30650  usgreghash2spot  30667  extwwlkfab  30688  numclwwlk5  30710  numclwwlk7  30712  lclkrs2  35190
  Copyright terms: Public domain W3C validator