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

Theorem cbvexv 1843
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 1464 . 2  |-  ( ph  ->  A. y ph )
2 ax-17 1464 . 2  |-  ( ps 
->  A. x ps )
3 cbvalv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvexh 1685 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103   E.wex 1426
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 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  eujust  1950  euind  2800  reuind  2818  r19.3rm  3366  r19.9rmv  3369  raaanlem  3383  raaan  3384  cbvopab2v  3907  bm1.3ii  3952  mss  4044  zfun  4252  xpiindim  4561  relop  4574  dmmrnm  4643  dmxpm  4644  dmcoss  4690  xpm  4840  cnviinm  4959  fv3  5312  fo1stresm  5914  fo2ndresm  5915  tfr1onlemaccex  6095  tfrcllemaccex  6108  iinerm  6344  riinerm  6345  ac6sfi  6594  fodjuomnilemm  6780  ltexprlemdisj  7144  ltexprlemloc  7145  recexprlemdisj  7168  zfz1isolem1  10210  climmo  10650  isummo  10737  bdbm1.3ii  11439
  Copyright terms: Public domain W3C validator