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

Theorem cbvexv 1870
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 1489 . 2  |-  ( ph  ->  A. y ph )
2 ax-17 1489 . 2  |-  ( ps 
->  A. x ps )
3 cbvalv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvexh 1711 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104   E.wex 1451
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  eujust  1977  euind  2842  reuind  2860  r19.2m  3417  r19.3rm  3419  r19.9rmv  3422  raaanlem  3436  raaan  3437  cbvopab2v  3973  bm1.3ii  4017  mss  4116  zfun  4324  xpiindim  4644  relop  4657  dmmrnm  4726  dmxpm  4727  dmcoss  4776  xpm  4928  cnviinm  5048  fv3  5410  fo1stresm  6025  fo2ndresm  6026  tfr1onlemaccex  6211  tfrcllemaccex  6224  iinerm  6467  riinerm  6468  ixpiinm  6584  ac6sfi  6758  ctmlemr  6959  ctm  6960  ctssdclemr  6963  ctssdc  6964  fodjum  6984  acfun  7027  ccfunen  7043  ltexprlemdisj  7378  ltexprlemloc  7379  recexprlemdisj  7402  suplocsr  7581  axpre-suploc  7674  zfz1isolem1  10534  climmo  11018  summodc  11103  ctiunct  11859  neipsm  12229  suplociccex  12678  bdbm1.3ii  12923
  Copyright terms: Public domain W3C validator