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

Theorem spcev 2888
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 2882 . 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 1531    = wceq 1632    e. wcel 1696   _Vcvv 2801
This theorem is referenced by:  dtruALT  4223  elALT  4234  dtruALT2  4235  nnullss  4251  exss  4252  euotd  4283  snnex  4540  opeldm  4898  elrnmpt1  4944  xpnz  5115  ffoss  5521  ssimaex  5600  fvelrn  5677  dff3  5689  exfo  5694  eufnfv  5768  elunirnALT  5795  foeqcnvco  5820  op1steq  6180  frxp  6241  seqomlem2  6479  domtr  6930  ensn1  6941  en1  6944  php3  7063  1sdom  7081  isinf  7092  ssfi  7099  ac6sfi  7117  hartogslem1  7273  brwdom2  7303  inf0  7338  axinf2  7357  cnfcom3clem  7424  tz9.1  7427  tz9.1c  7428  rankuni  7551  scott0  7572  cplem2  7576  bnd2  7579  karden  7581  cardprclem  7628  dfac4  7765  dfac5lem5  7770  dfac5  7771  dfac2a  7772  dfac2  7773  kmlem2  7793  kmlem13  7804  ackbij2  7885  cfsuc  7899  cfflb  7901  cfss  7907  cfsmolem  7912  cfcoflem  7914  fin23lem32  7986  axcc2lem  8078  axcc3  8080  axdc2lem  8090  axdc3lem2  8093  axcclem  8099  brdom3  8169  brdom7disj  8172  brdom6disj  8173  axpowndlem3  8237  canthnumlem  8286  canthp1lem2  8291  inar1  8413  recmulnq  8604  ltexnq  8615  halfnq  8616  ltbtwnnq  8618  1idpr  8669  ltexprlem7  8682  reclem2pr  8688  reclem3pr  8689  sup2  9726  nnunb  9977  uzrdgfni  11037  axdc4uzlem  11060  cnso  12541  vdwapun  13037  vdwlem1  13044  vdwlem12  13055  vdwlem13  13056  isacs2  13571  efglem  15041  cmpsublem  17142  cmpsub  17143  1stcfb  17187  alexsubALTlem3  17759  alexsubALTlem4  17760  vitali  18984  mbfi1fseqlem6  19091  mbfi1flimlem  19093  aannenlem2  19725  rtrclreclem.trans  24058  trpredpred  24302  elfix  24514  dffix2  24516  fnsingle  24529  axlowdim  24661  itg2addnclem  25003  itg2addnc  25005  vxveqv  25157  prj1b  25182  prj3  25183  dmrngcmp  25854  infemb  25962  finminlem  26334  filnetlem3  26432  indexdom  26516  sdclem2  26555  fdc  26558  prtlem16  26840  eldioph2lem2  26943  dford3lem2  27223  aomclem7  27260  dfac11  27263  enfixsn  27360  lmisfree  27415  psgneu  27532  fnchoice  27803  stoweidlem28  27880  bnj150  29224  dihglblem2aN  32105
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803
  Copyright terms: Public domain W3C validator