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

Theorem cbvex 1714
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 1484 . 2  |-  ( ph  ->  A. y ph )
3 cbvex.2 . . 3  |-  F/ x ps
43nfri 1484 . 2  |-  ( ps 
->  A. x ps )
5 cbvex.3 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
62, 4, 5cbvexh 1713 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104   F/wnf 1421   E.wex 1453
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 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499
This theorem depends on definitions:  df-bi 116  df-nf 1422
This theorem is referenced by:  sb8e  1813  cbvex2  1874  cbvmo  2017  mo23  2018  clelab  2242  cbvrexf  2626  issetf  2667  eqvincf  2784  rexab2  2823  cbvrexcsf  3033  abn0m  3358  rabn0m  3360  euabsn  3563  eluniab  3718  cbvopab1  3971  cbvopab2  3972  cbvopab1s  3973  intexabim  4047  iinexgm  4049  opeliunxp  4564  dfdmf  4702  dfrnf  4750  elrnmpt1  4760  cbvoprab1  5811  cbvoprab2  5812  opabex3d  5987  opabex3  5988  seq3f1olemp  10243  fsum2dlemstep  11171  bdsepnfALT  13014  strcollnfALT  13111
  Copyright terms: Public domain W3C validator