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

Theorem cbvexv 1943
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
cbvalv.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvexv  |-  ( E. x ph  <->  E. y ps )
Distinct variable groups:    ph, y    ps, x
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem cbvexv
StepHypRef Expression
1 nfv 1605 . 2  |-  F/ y
ph
2 nfv 1605 . 2  |-  F/ x ps
3 cbvalv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvex 1925 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   E.wex 1528
This theorem is referenced by:  eujust  2145  euind  2952  reuind  2968  cbvopab2v  4093  bm1.3ii  4144  zfun  4513  reusv2lem2  4536  relop  4834  dmcoss  4944  fv3  5541  exfo  5678  ac6sfi  7101  brwdom2  7287  aceq1  7744  aceq0  7745  aceq3lem  7747  dfac4  7749  kmlem2  7777  kmlem13  7788  axdc4lem  8081  zfac  8086  zfcndun  8237  zfcndac  8241  sup2  9710  supmul  9722  climmo  12031  summo  12190  gsumval3eu  15190  elpt  17267  wfrlem1  24256  frrlem1  24281  bpolyval  24784  fdc  26455  ax10ext  27606  fnchoice  27700  bnj1185  28826
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator