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

Theorem spcev 2780
Description: Existential specialization, using implicit substitution. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
Hypotheses
Ref Expression
spcv.1  |-  A  e. 
_V
spcv.2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
spcev  |-  ( ps 
->  E. x ph )
Distinct variable groups:    x, A    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem spcev
StepHypRef Expression
1 spcv.1 . 2  |-  A  e. 
_V
2 spcv.2 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
32spcegv 2774 . 2  |-  ( A  e.  _V  ->  ( ps  ->  E. x ph )
)
41, 3ax-mp 5 1  |-  ( ps 
->  E. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    = wceq 1331   E.wex 1468    e. wcel 1480   _Vcvv 2686
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-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688
This theorem is referenced by:  bnd2  4097  mss  4148  exss  4149  snnex  4369  opeldm  4742  elrnmpt1  4790  xpmlem  4959  ffoss  5399  ssimaex  5482  fvelrn  5551  eufnfv  5648  foeqcnvco  5691  cnvoprab  6131  domtr  6679  ensn1  6690  ac6sfi  6792  difinfsn  6985  0ct  6992  ctmlemr  6993  ctssdclemn0  6995  ctssdclemr  6997  ctssdc  6998  omct  7002  ctssexmid  7024  exmidfodomrlemim  7057  cc3  7083  zfz1iso  10591  ennnfonelemim  11943  ctinfom  11947  ctinf  11949  qnnen  11950  enctlem  11951  ctiunct  11959  subctctexmid  13249
  Copyright terms: Public domain W3C validator