MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  spcev Unicode version

Theorem spcev 3003
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 2997 . 2  |-  ( A  e.  _V  ->  ( ps  ->  E. x ph )
)
41, 3ax-mp 8 1  |-  ( ps 
->  E. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   E.wex 1547    = wceq 1649    e. wcel 1721   _Vcvv 2916
This theorem is referenced by:  dtruALT  4356  elALT  4367  dtruALT2  4368  nnullss  4385  exss  4386  euotd  4417  snnex  4672  opeldm  5032  elrnmpt1  5078  xpnz  5251  ffoss  5666  ssimaex  5747  fvelrn  5825  dff3  5841  exfo  5846  eufnfv  5931  elunirnALT  5959  foeqcnvco  5986  op1steq  6350  frxp  6415  seqomlem2  6667  domtr  7119  ensn1  7130  en1  7133  php3  7252  1sdom  7270  isinf  7281  ssfi  7288  ac6sfi  7310  hartogslem1  7467  brwdom2  7497  inf0  7532  axinf2  7551  cnfcom3clem  7618  tz9.1  7621  tz9.1c  7622  rankuni  7745  scott0  7766  cplem2  7770  bnd2  7773  karden  7775  cardprclem  7822  dfac4  7959  dfac5lem5  7964  dfac5  7965  dfac2a  7966  dfac2  7967  kmlem2  7987  kmlem13  7998  ackbij2  8079  cfsuc  8093  cfflb  8095  cfss  8101  cfsmolem  8106  cfcoflem  8108  fin23lem32  8180  axcc2lem  8272  axcc3  8274  axdc2lem  8284  axdc3lem2  8287  axcclem  8293  brdom3  8362  brdom7disj  8365  brdom6disj  8366  axpowndlem3  8430  canthnumlem  8479  canthp1lem2  8484  inar1  8606  recmulnq  8797  ltexnq  8808  halfnq  8809  ltbtwnnq  8811  1idpr  8862  ltexprlem7  8875  reclem2pr  8881  reclem3pr  8882  sup2  9920  nnunb  10173  uzrdgfni  11253  axdc4uzlem  11276  cnso  12801  vdwapun  13297  vdwlem1  13304  vdwlem12  13315  vdwlem13  13316  isacs2  13833  efglem  15303  neitr  17198  cmpsublem  17416  cmpsub  17417  1stcfb  17461  alexsubALTlem3  18033  alexsubALTlem4  18034  vitali  19458  mbfi1fseqlem6  19565  mbfi1flimlem  19567  aannenlem2  20199  rtrclreclem.trans  25099  ntrivcvgmullem  25182  fprodntriv  25221  trpredpred  25445  elfix  25657  dffix2  25659  fnsingle  25672  axlowdim  25804  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  itg2addnclem  26155  itg2addnc  26158  finminlem  26211  filnetlem3  26299  indexdom  26326  sdclem2  26336  fdc  26339  prtlem16  26608  eldioph2lem2  26709  dford3lem2  26988  aomclem7  27025  dfac11  27028  enfixsn  27125  lmisfree  27180  psgneu  27297  fnchoice  27567  stoweidlem28  27644  bnj150  28953  dihglblem2aN  31776
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918
  Copyright terms: Public domain W3C validator