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

Theorem cbvrabv 2961
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 2569 . 2  |-  F/_ x A
2 nfcv 2569 . 2  |-  F/_ y A
3 nfv 1672 . 2  |-  F/ y
ph
4 nfv 1672 . 2  |-  F/ x ps
5 cbvrabv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
61, 2, 3, 4, 5cbvrab 2960 1  |-  { x  e.  A  |  ph }  =  { y  e.  A  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1362   {crab 2709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rab 2714
This theorem is referenced by:  pwnss  4445  knatar  6035  oeeulem  7028  ordtypecbv  7719  ordtypelem9  7728  inf3lema  7818  oemapso  7878  oemapvali  7880  tz9.12lem3  7984  cofsmo  8426  enfin2i  8478  fin23lem33  8502  isf32lem11  8520  zorn2g  8660  pwfseqlem1  8812  pwfseqlem3  8814  zsupss  10931  zmin  10936  reexALT  10972  hashbc  12189  sqrlem7  12721  rpnnen  13491  divalglem5  13583  bitsfzolem  13612  smupp1  13658  gcdcllem3  13679  bezout  13708  eulerth  13840  odzval  13845  pcprecl  13888  pcprendvds  13889  pcpremul  13892  pceulem  13894  prmreclem1  13959  prmreclem5  13963  prmreclem6  13964  4sqlem19  14006  vdwnn  14041  hashbcval  14045  gsumvalx  15483  symgfixelq  15917  efgsdm  16206  efgsfo  16215  ablfaclem3  16561  ltbwe  17485  coe1mul2lem2  17619  smadiadetlem3  18315  pptbas  18453  concompss  18878  ptcmplem5  19469  ustuqtop  19662  utopsnneip  19664  icccmplem2  20241  minveclem5  20761  ivth  20779  ovolicc2lem5  20845  ovolicc  20847  opnmbllem  20922  vitali  20934  itg2monolem3  21071  elqaa  21672  radcnvle  21769  pserdvlem2  21777  wilth  22293  ftalem6  22299  ttgval  22943  axcontlem11  23042  nbgraf1olem1  23172  nbgraf1o  23178  cusgraexg  23199  cusgrafi  23212  ubthlem3  24095  htth  24142  ordtconlem1  26207  ddemeas  26505  oddpwdc  26584  eulerpartgbij  26602  eulerpartlemn  26611  eulerpart  26612  ballotlemelo  26717  ballotleme  26726  ballotlem7  26765  lgamgulmlem5  26866  lgamcvglem  26873  subfacp1lem6  26920  erdsze  26937  cvmscbv  26994  cvmsiota  27013  cvmlift2lem13  27051  mblfinlem1  28269  mblfinlem2  28270  neibastop2  28423  eldioph4i  28993  stoweidlem49  29687  wrd2f1tovbij  30098  wlknwwlknbij2  30189  wlkiswwlkbij2  30196  wwlkextbij  30208  wlknwwlknvbij  30215  clwwlkvbij  30306  Lemma2  30336  hashecclwwlkn1  30351  usghashecclwwlk  30352  clwlksizeeq  30368  rusgranumwlklem4  30413  rusgranumwlks  30417  frgraregorufr0  30488  usgreghash2spot  30505  extwwlkfab  30526  numclwwlk5  30548  numclwwlk7  30550  lclkrs2  34755
  Copyright terms: Public domain W3C validator