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

Theorem spcev 3035
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 3029 . 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 1550    = wceq 1652    e. wcel 1725   _Vcvv 2948
This theorem is referenced by:  dtruALT  4388  elALT  4399  dtruALT2  4400  nnullss  4417  exss  4418  euotd  4449  snnex  4704  opeldm  5064  elrnmpt1  5110  xpnz  5283  ffoss  5698  ssimaex  5779  fvelrn  5857  dff3  5873  exfo  5878  eufnfv  5963  elunirnALT  5991  foeqcnvco  6018  op1steq  6382  frxp  6447  seqomlem2  6699  domtr  7151  ensn1  7162  en1  7165  php3  7284  1sdom  7302  isinf  7313  ssfi  7320  ac6sfi  7342  hartogslem1  7500  brwdom2  7530  inf0  7565  axinf2  7584  cnfcom3clem  7651  tz9.1  7654  tz9.1c  7655  rankuni  7778  scott0  7799  cplem2  7803  bnd2  7806  karden  7808  cardprclem  7855  dfac4  7992  dfac5lem5  7997  dfac5  7998  dfac2a  7999  dfac2  8000  kmlem2  8020  kmlem13  8031  ackbij2  8112  cfsuc  8126  cfflb  8128  cfss  8134  cfsmolem  8139  cfcoflem  8141  fin23lem32  8213  axcc2lem  8305  axcc3  8307  axdc2lem  8317  axdc3lem2  8320  axcclem  8326  brdom3  8395  brdom7disj  8398  brdom6disj  8399  axpowndlem3  8463  canthnumlem  8512  canthp1lem2  8517  inar1  8639  recmulnq  8830  ltexnq  8841  halfnq  8842  ltbtwnnq  8844  1idpr  8895  ltexprlem7  8908  reclem2pr  8914  reclem3pr  8915  sup2  9953  nnunb  10206  uzrdgfni  11286  axdc4uzlem  11309  cnso  12834  vdwapun  13330  vdwlem1  13337  vdwlem12  13348  vdwlem13  13349  isacs2  13866  efglem  15336  neitr  17232  cmpsublem  17450  cmpsub  17451  1stcfb  17496  alexsubALTlem3  18068  alexsubALTlem4  18069  vitali  19493  mbfi1fseqlem6  19600  mbfi1flimlem  19602  aannenlem2  20234  rtrclreclem.trans  25134  ntrivcvgmullem  25218  fprodntriv  25257  trpredpred  25486  elfix  25698  dffix2  25700  fnsingle  25714  axlowdim  25848  mblfinlem2  26191  mblfinlem3  26192  ismblfin  26193  itg2addnclem  26202  itg2addnc  26205  finminlem  26258  filnetlem3  26346  indexdom  26373  sdclem2  26383  fdc  26386  prtlem16  26655  eldioph2lem2  26756  dford3lem2  27035  aomclem7  27072  dfac11  27075  enfixsn  27172  lmisfree  27227  psgneu  27344  fnchoice  27614  stoweidlem28  27691  bnj150  29101  dihglblem2aN  31930
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950
  Copyright terms: Public domain W3C validator