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

Theorem cbvex 1730
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 1500 . 2  |-  ( ph  ->  A. y ph )
3 cbvex.2 . . 3  |-  F/ x ps
43nfri 1500 . 2  |-  ( ps 
->  A. x ps )
5 cbvex.3 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
62, 4, 5cbvexh 1729 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104   F/wnf 1437   E.wex 1469
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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515
This theorem depends on definitions:  df-bi 116  df-nf 1438
This theorem is referenced by:  sb8e  1830  cbvex2  1895  cbvmo  2040  mo23  2041  clelab  2266  cbvrexf  2652  issetf  2696  eqvincf  2814  rexab2  2854  cbvrexcsf  3068  abn0m  3393  rabn0m  3395  euabsn  3601  eluniab  3756  cbvopab1  4009  cbvopab2  4010  cbvopab1s  4011  intexabim  4085  iinexgm  4087  opeliunxp  4602  dfdmf  4740  dfrnf  4788  elrnmpt1  4798  cbvoprab1  5851  cbvoprab2  5852  opabex3d  6027  opabex3  6028  seq3f1olemp  10306  fsum2dlemstep  11235  bdsepnfALT  13258  strcollnfALT  13355
  Copyright terms: Public domain W3C validator