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

Theorem cbvex 1756
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 1519 . 2  |-  ( ph  ->  A. y ph )
3 cbvex.2 . . 3  |-  F/ x ps
43nfri 1519 . 2  |-  ( ps 
->  A. x ps )
5 cbvex.3 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
62, 4, 5cbvexh 1755 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105   F/wnf 1460   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  df-nf 1461
This theorem is referenced by:  sb8e  1857  cbvex2  1922  cbvmo  2066  mo23  2067  clelab  2303  cbvrexf  2697  issetf  2744  eqvincf  2862  rexab2  2903  cbvrexcsf  3120  abn0m  3448  rabn0m  3450  euabsn  3662  eluniab  3821  cbvopab1  4075  cbvopab2  4076  cbvopab1s  4077  intexabim  4151  iinexgm  4153  opeliunxp  4680  dfdmf  4818  dfrnf  4866  elrnmpt1  4876  cbvoprab1  5943  cbvoprab2  5944  opabex3d  6118  opabex3  6119  seq3f1olemp  10496  fsum2dlemstep  11434  bdsepnfALT  14492  strcollnfALT  14589
  Copyright terms: Public domain W3C validator