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

Theorem spcev 2875
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 2869 . 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 176   E.wex 1528    = wceq 1623    e. wcel 1684   _Vcvv 2788
This theorem is referenced by:  dtruALT  4207  elALT  4218  dtruALT2  4219  nnullss  4235  exss  4236  euotd  4267  snnex  4524  opeldm  4882  elrnmpt1  4928  xpnz  5099  ffoss  5505  ssimaex  5584  fvelrn  5661  dff3  5673  exfo  5678  eufnfv  5752  elunirnALT  5779  foeqcnvco  5804  op1steq  6164  frxp  6225  seqomlem2  6463  domtr  6914  ensn1  6925  en1  6928  php3  7047  1sdom  7065  isinf  7076  ssfi  7083  ac6sfi  7101  hartogslem1  7257  brwdom2  7287  inf0  7322  axinf2  7341  cnfcom3clem  7408  tz9.1  7411  tz9.1c  7412  rankuni  7535  scott0  7556  cplem2  7560  bnd2  7563  karden  7565  cardprclem  7612  dfac4  7749  dfac5lem5  7754  dfac5  7755  dfac2a  7756  dfac2  7757  kmlem2  7777  kmlem13  7788  ackbij2  7869  cfsuc  7883  cfflb  7885  cfss  7891  cfsmolem  7896  cfcoflem  7898  fin23lem32  7970  axcc2lem  8062  axcc3  8064  axdc2lem  8074  axdc3lem2  8077  axcclem  8083  brdom3  8153  brdom7disj  8156  brdom6disj  8157  axpowndlem3  8221  canthnumlem  8270  canthp1lem2  8275  inar1  8397  recmulnq  8588  ltexnq  8599  halfnq  8600  ltbtwnnq  8602  1idpr  8653  ltexprlem7  8666  reclem2pr  8672  reclem3pr  8673  sup2  9710  nnunb  9961  uzrdgfni  11021  axdc4uzlem  11044  cnso  12525  vdwapun  13021  vdwlem1  13028  vdwlem12  13039  vdwlem13  13040  isacs2  13555  efglem  15025  cmpsublem  17126  cmpsub  17127  1stcfb  17171  alexsubALTlem3  17743  alexsubALTlem4  17744  vitali  18968  mbfi1fseqlem6  19075  mbfi1flimlem  19077  aannenlem2  19709  rtrclreclem.trans  24043  trpredpred  24231  elfix  24443  dffix2  24445  fnsingle  24458  axlowdim  24589  vxveqv  25054  prj1b  25079  prj3  25080  dmrngcmp  25751  infemb  25859  finminlem  26231  filnetlem3  26329  indexdom  26413  sdclem2  26452  fdc  26455  prtlem16  26737  eldioph2lem2  26840  dford3lem2  27120  aomclem7  27157  dfac11  27160  enfixsn  27257  lmisfree  27312  psgneu  27429  fnchoice  27700  stoweidlem28  27777  bnj150  28908  dihglblem2aN  31483
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790
  Copyright terms: Public domain W3C validator