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

Theorem cbvex 1681
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 1453 . 2  |-  ( ph  ->  A. y ph )
3 cbvex.2 . . 3  |-  F/ x ps
43nfri 1453 . 2  |-  ( ps 
->  A. x ps )
5 cbvex.3 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
62, 4, 5cbvexh 1680 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103   F/wnf 1390   E.wex 1422
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468
This theorem depends on definitions:  df-bi 115  df-nf 1391
This theorem is referenced by:  sb8e  1780  cbvex2  1840  cbvmo  1983  mo23  1984  clelab  2207  cbvrexf  2577  issetf  2615  eqvincf  2728  rexab2  2767  cbvrexcsf  2974  rabn0m  3288  euabsn  3480  eluniab  3633  cbvopab1  3871  cbvopab2  3872  cbvopab1s  3873  intexabim  3947  iinexgm  3949  opeliunxp  4441  dfdmf  4576  dfrnf  4623  elrnmpt1  4633  cbvoprab1  5627  cbvoprab2  5628  opabex3d  5799  opabex3  5800  bdsepnfALT  10947  strcollnfALT  11048
  Copyright terms: Public domain W3C validator