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

Theorem ceqsexv 2639
Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.)
Hypotheses
Ref Expression
ceqsexv.1  |-  A  e. 
_V
ceqsexv.2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
ceqsexv  |-  ( E. x ( x  =  A  /\  ph )  <->  ps )
Distinct variable groups:    x, A    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem ceqsexv
StepHypRef Expression
1 nfv 1462 . 2  |-  F/ x ps
2 ceqsexv.1 . 2  |-  A  e. 
_V
3 ceqsexv.2 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3ceqsex 2638 1  |-  ( E. x ( x  =  A  /\  ph )  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103    = wceq 1285   E.wex 1422    e. wcel 1434   _Vcvv 2602
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-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-v 2604
This theorem is referenced by:  ceqsex3v  2642  gencbvex  2646  sbhypf  2649  euxfr2dc  2778  inuni  3938  eqvinop  4006  onm  4164  uniuni  4209  opeliunxp  4421  elvvv  4429  rexiunxp  4506  imai  4711  coi1  4866  abrexco  5430  opabex3d  5779  opabex3  5780  xpsnen  6365  xpcomco  6370  xpassen  6374
  Copyright terms: Public domain W3C validator