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

Theorem spcev 2987
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 2981 . 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 1717   _Vcvv 2900
This theorem is referenced by:  dtruALT  4338  elALT  4349  dtruALT2  4350  nnullss  4367  exss  4368  euotd  4399  snnex  4654  opeldm  5014  elrnmpt1  5060  xpnz  5233  ffoss  5648  ssimaex  5728  fvelrn  5806  dff3  5822  exfo  5827  eufnfv  5912  elunirnALT  5940  foeqcnvco  5967  op1steq  6331  frxp  6393  seqomlem2  6645  domtr  7097  ensn1  7108  en1  7111  php3  7230  1sdom  7248  isinf  7259  ssfi  7266  ac6sfi  7288  hartogslem1  7445  brwdom2  7475  inf0  7510  axinf2  7529  cnfcom3clem  7596  tz9.1  7599  tz9.1c  7600  rankuni  7723  scott0  7744  cplem2  7748  bnd2  7751  karden  7753  cardprclem  7800  dfac4  7937  dfac5lem5  7942  dfac5  7943  dfac2a  7944  dfac2  7945  kmlem2  7965  kmlem13  7976  ackbij2  8057  cfsuc  8071  cfflb  8073  cfss  8079  cfsmolem  8084  cfcoflem  8086  fin23lem32  8158  axcc2lem  8250  axcc3  8252  axdc2lem  8262  axdc3lem2  8265  axcclem  8271  brdom3  8340  brdom7disj  8343  brdom6disj  8344  axpowndlem3  8408  canthnumlem  8457  canthp1lem2  8462  inar1  8584  recmulnq  8775  ltexnq  8786  halfnq  8787  ltbtwnnq  8789  1idpr  8840  ltexprlem7  8853  reclem2pr  8859  reclem3pr  8860  sup2  9897  nnunb  10150  uzrdgfni  11226  axdc4uzlem  11249  cnso  12774  vdwapun  13270  vdwlem1  13277  vdwlem12  13288  vdwlem13  13289  isacs2  13806  efglem  15276  neitr  17167  cmpsublem  17385  cmpsub  17386  1stcfb  17430  alexsubALTlem3  18002  alexsubALTlem4  18003  vitali  19373  mbfi1fseqlem6  19480  mbfi1flimlem  19482  aannenlem2  20114  rtrclreclem.trans  24926  ntrivcvgmullem  25009  fprodntriv  25048  trpredpred  25256  elfix  25468  dffix2  25470  fnsingle  25483  axlowdim  25615  itg2addnclem  25958  itg2addnc  25960  finminlem  26013  filnetlem3  26101  indexdom  26128  sdclem2  26138  fdc  26141  prtlem16  26410  eldioph2lem2  26511  dford3lem2  26790  aomclem7  26827  dfac11  26830  enfixsn  26927  lmisfree  26982  psgneu  27099  fnchoice  27369  stoweidlem28  27446  bnj150  28586  dihglblem2aN  31409
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902
  Copyright terms: Public domain W3C validator