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

Theorem cbvex 1744
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
cbvex.1  |-  F/ y
ph
cbvex.2  |-  F/ x ps
cbvex.3  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvex  |-  ( E. x ph  <->  E. y ps )

Proof of Theorem cbvex
StepHypRef Expression
1 cbvex.1 . . 3  |-  F/ y
ph
21nfri 1507 . 2  |-  ( ph  ->  A. y ph )
3 cbvex.2 . . 3  |-  F/ x ps
43nfri 1507 . 2  |-  ( ps 
->  A. x ps )
5 cbvex.3 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
62, 4, 5cbvexh 1743 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104   F/wnf 1448   E.wex 1480
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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522
This theorem depends on definitions:  df-bi 116  df-nf 1449
This theorem is referenced by:  sb8e  1845  cbvex2  1910  cbvmo  2054  mo23  2055  clelab  2292  cbvrexf  2686  issetf  2733  eqvincf  2851  rexab2  2892  cbvrexcsf  3108  abn0m  3434  rabn0m  3436  euabsn  3646  eluniab  3801  cbvopab1  4055  cbvopab2  4056  cbvopab1s  4057  intexabim  4131  iinexgm  4133  opeliunxp  4659  dfdmf  4797  dfrnf  4845  elrnmpt1  4855  cbvoprab1  5914  cbvoprab2  5915  opabex3d  6089  opabex3  6090  seq3f1olemp  10437  fsum2dlemstep  11375  bdsepnfALT  13771  strcollnfALT  13868
  Copyright terms: Public domain W3C validator