ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cbvexv Unicode version

Theorem cbvexv 1837
Description: Rule used to change bound variables, using implicit substitition. (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 ax-17 1460 . 2  |-  ( ph  ->  A. y ph )
2 ax-17 1460 . 2  |-  ( ps 
->  A. x ps )
3 cbvalv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvexh 1679 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103   E.wex 1422
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  eujust  1944  euind  2780  reuind  2796  r19.3rm  3337  r19.9rmv  3340  raaanlem  3354  raaan  3355  cbvopab2v  3863  bm1.3ii  3907  mss  3989  zfun  4197  xpiindim  4501  relop  4514  dmmrnm  4582  dmxpm  4583  dmcoss  4629  xpm  4775  cnviinm  4889  fv3  5229  fo1stresm  5819  fo2ndresm  5820  tfr1onlemaccex  5997  tfrcllemaccex  6010  iinerm  6244  riinerm  6245  ac6sfi  6431  ltexprlemdisj  6858  ltexprlemloc  6859  recexprlemdisj  6882  climmo  10275  bdbm1.3ii  10840
  Copyright terms: Public domain W3C validator