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

Theorem ceqsexv 2777
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 1528 . 2  |-  F/ x ps
2 ceqsexv.1 . 2  |-  A  e. 
_V
3 ceqsexv.2 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3ceqsex 2776 1  |-  ( E. x ( x  =  A  /\  ph )  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105    = wceq 1353   E.wex 1492    e. wcel 2148   _Vcvv 2738
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-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2740
This theorem is referenced by:  ceqsex3v  2780  gencbvex  2784  sbhypf  2787  euxfr2dc  2923  inuni  4156  eqvinop  4244  onm  4402  uniuni  4452  opeliunxp  4682  elvvv  4690  rexiunxp  4770  imai  4985  coi1  5145  abrexco  5760  opabex3d  6122  opabex3  6123  mapsnen  6811  xpsnen  6821  xpcomco  6826  xpassen  6830
  Copyright terms: Public domain W3C validator