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

Theorem spcev 3052
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 3046 . 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 178   E.wex 1551    = wceq 1654    e. wcel 1728   _Vcvv 2965
This theorem is referenced by:  dtruALT  4431  elALT  4442  dtruALT2  4443  nnullss  4460  exss  4461  euotd  4492  snnex  4748  opeldm  5108  elrnmpt1  5154  xpnz  5327  ffoss  5742  ssimaex  5824  fvelrn  5902  dff3  5918  exfo  5923  eufnfv  6008  elunirnALT  6036  foeqcnvco  6063  op1steq  6427  frxp  6492  seqomlem2  6744  domtr  7196  ensn1  7207  en1  7210  php3  7329  1sdom  7347  isinf  7358  ssfi  7365  ac6sfi  7387  hartogslem1  7547  brwdom2  7577  inf0  7612  axinf2  7631  cnfcom3clem  7698  tz9.1  7701  tz9.1c  7702  rankuni  7825  scott0  7848  cplem2  7852  bnd2  7855  karden  7857  cardprclem  7904  dfac4  8041  dfac5lem5  8046  dfac5  8047  dfac2a  8048  dfac2  8049  kmlem2  8069  kmlem13  8080  ackbij2  8161  cfsuc  8175  cfflb  8177  cfss  8183  cfsmolem  8188  cfcoflem  8190  fin23lem32  8262  axcc2lem  8354  axcc3  8356  axdc2lem  8366  axdc3lem2  8369  axcclem  8375  brdom3  8444  brdom7disj  8447  brdom6disj  8448  axpowndlem3  8512  canthnumlem  8561  canthp1lem2  8566  inar1  8688  recmulnq  8879  ltexnq  8890  halfnq  8891  ltbtwnnq  8893  1idpr  8944  ltexprlem7  8957  reclem2pr  8963  reclem3pr  8964  sup2  10002  nnunb  10255  uzrdgfni  11336  axdc4uzlem  11359  cnso  12884  vdwapun  13380  vdwlem1  13387  vdwlem12  13398  vdwlem13  13399  isacs2  13916  efglem  15386  neitr  17282  cmpsublem  17500  cmpsub  17501  1stcfb  17546  alexsubALTlem3  18118  alexsubALTlem4  18119  vitali  19543  mbfi1fseqlem6  19648  mbfi1flimlem  19650  aannenlem2  20284  rtrclreclem.trans  25181  ntrivcvgmullem  25264  fprodntriv  25303  trpredpred  25541  fnsingle  25799  axlowdim  25935  mblfinlem3  26285  mblfinlem4  26286  ismblfin  26287  itg2addnclem  26298  itg2addnc  26301  finminlem  26363  filnetlem3  26451  indexdom  26478  sdclem2  26488  fdc  26491  prtlem16  26830  eldioph2lem2  26931  dford3lem2  27210  aomclem7  27247  dfac11  27249  enfixsn  27346  lmisfree  27401  psgneu  27518  fnchoice  27788  stoweidlem28  27865  bnj150  29421  dihglblem2aN  32265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-v 2967
  Copyright terms: Public domain W3C validator