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

Theorem cbvexv 2010
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 1694 . 2  |-  F/ y
ph
2 nfv 1694 . 2  |-  F/ x ps
3 cbvalv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvex 2008 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E.wex 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-nf 1604
This theorem is referenced by:  eujust  2270  euind  3272  reuind  3289  cbvopab2v  4511  bm1.3ii  4561  reusv2lem2  4639  relop  5143  dmcoss  5252  fv3  5869  exfo  6034  zfun  6578  ac6sfi  7766  brwdom2  8002  aceq1  8501  aceq0  8502  aceq3lem  8504  dfac4  8506  kmlem2  8534  kmlem13  8545  axdc4lem  8838  zfac  8843  zfcndun  8996  zfcndac  9000  sup2  10506  supmul  10518  climmo  13362  summo  13521  prodmo  13725  gsumval3eu  16886  elpt  20051  usgraedg4  24365  wfrlem1  29319  frrlem1  29363  fdc  30214  axc11next  31267  fnchoice  31358  bnj1185  33720
  Copyright terms: Public domain W3C validator