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

Theorem cbvexv 1918
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 1526 . 2  |-  ( ph  ->  A. y ph )
2 ax-17 1526 . 2  |-  ( ps 
->  A. x ps )
3 cbvalv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvexh 1755 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105   E.wex 1492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  eujust  2028  euind  2925  reuind  2943  r19.2m  3510  r19.3rm  3512  r19.9rmv  3515  raaanlem  3529  raaan  3530  cbvopab2v  4081  bm1.3ii  4125  mss  4227  zfun  4435  xpiindim  4765  relop  4778  dmmrnm  4847  dmxpm  4848  dmcoss  4897  xpm  5051  cnviinm  5171  iotam  5209  fv3  5539  fo1stresm  6162  fo2ndresm  6163  tfr1onlemaccex  6349  tfrcllemaccex  6362  iinerm  6607  riinerm  6608  ixpiinm  6724  ac6sfi  6898  ctmlemr  7107  ctm  7108  ctssdclemr  7111  ctssdc  7112  fodjum  7144  acfun  7206  ccfunen  7263  cc2lem  7265  cc2  7266  ltexprlemdisj  7605  ltexprlemloc  7606  recexprlemdisj  7629  suplocsr  7808  axpre-suploc  7901  zfz1isolem1  10820  climmo  11306  summodc  11391  nninfdcex  11954  zsupssdc  11955  ctiunct  12441  ismnd  12820  dfgrp3me  12970  issubg2m  13049  subrgintm  13364  neipsm  13657  suplociccex  14106  bdbm1.3ii  14646
  Copyright terms: Public domain W3C validator