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

Theorem cbvexv 1997
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 21-Jun-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 1683 . 2  |-  F/ y
ph
2 nfv 1683 . 2  |-  F/ x ps
3 cbvalv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvex 1995 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E.wex 1596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600
This theorem is referenced by:  eujust  2277  euind  3290  reuind  3307  cbvopab2v  4521  bm1.3ii  4571  reusv2lem2  4649  relop  5151  dmcoss  5260  fv3  5877  exfo  6037  zfun  6575  ac6sfi  7760  brwdom2  7995  aceq1  8494  aceq0  8495  aceq3lem  8497  dfac4  8499  kmlem2  8527  kmlem13  8538  axdc4lem  8831  zfac  8836  zfcndun  8989  zfcndac  8993  sup2  10495  supmul  10507  climmo  13339  summo  13498  gsumval3eu  16698  elpt  19808  usgraedg4  24063  prodmo  28645  wfrlem1  28920  frrlem1  28964  fdc  29841  axc11next  30891  fnchoice  30982  bnj1185  32931
  Copyright terms: Public domain W3C validator