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

Theorem spcev 3440
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 𝐴 ∈ V
spcv.2 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
spcev (𝜓 → ∃𝑥𝜑)
Distinct variable groups:   𝑥,𝐴   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem spcev
StepHypRef Expression
1 spcv.1 . 2 𝐴 ∈ V
2 spcv.2 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32spcegv 3434 . 2 (𝐴 ∈ V → (𝜓 → ∃𝑥𝜑))
41, 3ax-mp 5 1 (𝜓 → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1632  wex 1853  wcel 2139  Vcvv 3340
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342
This theorem is referenced by:  dtruALT  5048  elALT  5059  dtruALT2  5060  nnullss  5079  exss  5080  euotd  5123  opeldm  5483  elrnmpt1  5529  xpnz  5711  ssimaex  6425  fvelrn  6515  dff3  6535  exfo  6540  eufnfv  6654  elunirn  6672  fsnex  6701  f1prex  6702  foeqcnvco  6718  snnexOLD  7132  ffoss  7292  op1steq  7377  frxp  7455  suppimacnv  7474  seqomlem2  7715  domtr  8174  ensn1  8185  en1  8188  enfixsn  8234  php3  8311  1sdom  8328  isinf  8338  ssfi  8345  ac6sfi  8369  hartogslem1  8612  brwdom2  8643  inf0  8691  axinf2  8710  cnfcom3clem  8775  tz9.1  8778  tz9.1c  8779  rankuni  8899  scott0  8922  cplem2  8926  bnd2  8929  karden  8931  cardprclem  8995  dfac4  9135  dfac5lem5  9140  dfac5  9141  dfac2a  9142  dfac2b  9143  dfac2OLD  9145  kmlem2  9165  kmlem13  9176  ackbij2  9257  cfsuc  9271  cfflb  9273  cfss  9279  cfsmolem  9284  cfcoflem  9286  fin23lem32  9358  axcc2lem  9450  axcc3  9452  axdc2lem  9462  axdc3lem2  9465  axcclem  9471  brdom3  9542  brdom7disj  9545  brdom6disj  9546  axpowndlem3  9613  canthnumlem  9662  canthp1lem2  9667  inar1  9789  recmulnq  9978  ltexnq  9989  halfnq  9990  ltbtwnnq  9992  1idpr  10043  ltexprlem7  10056  reclem2pr  10062  reclem3pr  10063  sup2  11171  nnunb  11480  uzrdgfni  12951  axdc4uzlem  12976  rtrclreclem3  13999  ntrivcvgmullem  14832  fprodntriv  14871  cnso  15175  vdwapun  15880  vdwlem1  15887  vdwlem12  15898  vdwlem13  15899  isacs2  16515  equivestrcsetc  16993  psgneu  18126  efglem  18329  lmisfree  20383  toprntopon  20931  neitr  21186  cmpsublem  21404  cmpsub  21405  bwth  21415  1stcfb  21450  unisngl  21532  alexsubALTlem3  22054  alexsubALTlem4  22055  vitali  23581  mbfi1fseqlem6  23686  mbfi1flimlem  23688  aannenlem2  24283  istrkg2ld  25558  axlowdim  26040  wlkpwwlkf1ouspgr  26988  wlkisowwlkupgr  26989  padct  29806  cnvoprabOLD  29807  f1ocnt  29868  locfinreflem  30216  locfinref  30217  prsdm  30269  prsrn  30270  eulerpart  30753  bnj150  31253  trpredpred  32033  nosupno  32155  nosupfv  32158  fnsingle  32332  finminlem  32618  filnetlem3  32681  cnndvlem2  32835  bj-restpw  33351  bj-rest0  33352  poimirlem2  33724  mblfinlem3  33761  mblfinlem4  33762  ismblfin  33763  itg2addnclem  33774  itg2addnc  33777  indexdom  33842  sdclem2  33851  fdc  33854  prtlem16  34658  dihglblem2aN  37084  eldioph2lem2  37826  dford3lem2  38096  aomclem7  38132  dfac11  38134  relintabex  38389  rclexi  38424  trclexi  38429  rtrclexi  38430  fnchoice  39687  ssnnf1octb  39881  fzisoeu  40013  stoweidlem28  40748  nnfoctbdjlem  41175  smfpimcclem  41519  setrec1lem3  42946  setrec2lem2  42951
  Copyright terms: Public domain W3C validator