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

Theorem spcev 3331
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 3325 . 2 (𝐴 ∈ V → (𝜓 → ∃𝑥𝜑))
41, 3ax-mp 5 1 (𝜓 → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wex 1744  wcel 2030  Vcvv 3231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233
This theorem is referenced by:  dtruALT  4929  elALT  4940  dtruALT2  4941  nnullss  4960  exss  4961  euotd  5004  opeldm  5360  elrnmpt1  5406  xpnz  5588  ssimaex  6302  fvelrn  6392  dff3  6412  exfo  6417  eufnfv  6531  elunirn  6549  fsnex  6578  f1prex  6579  foeqcnvco  6595  snnexOLD  7009  ffoss  7169  op1steq  7254  frxp  7332  suppimacnv  7351  seqomlem2  7591  domtr  8050  ensn1  8061  en1  8064  enfixsn  8110  php3  8187  1sdom  8204  isinf  8214  ssfi  8221  ac6sfi  8245  hartogslem1  8488  brwdom2  8519  inf0  8556  axinf2  8575  cnfcom3clem  8640  tz9.1  8643  tz9.1c  8644  rankuni  8764  scott0  8787  cplem2  8791  bnd2  8794  karden  8796  cardprclem  8843  dfac4  8983  dfac5lem5  8988  dfac5  8989  dfac2a  8990  dfac2  8991  kmlem2  9011  kmlem13  9022  ackbij2  9103  cfsuc  9117  cfflb  9119  cfss  9125  cfsmolem  9130  cfcoflem  9132  fin23lem32  9204  axcc2lem  9296  axcc3  9298  axdc2lem  9308  axdc3lem2  9311  axcclem  9317  brdom3  9388  brdom7disj  9391  brdom6disj  9392  axpowndlem3  9459  canthnumlem  9508  canthp1lem2  9513  inar1  9635  recmulnq  9824  ltexnq  9835  halfnq  9836  ltbtwnnq  9838  1idpr  9889  ltexprlem7  9902  reclem2pr  9908  reclem3pr  9909  sup2  11017  nnunb  11326  uzrdgfni  12797  axdc4uzlem  12822  rtrclreclem3  13844  ntrivcvgmullem  14677  fprodntriv  14716  cnso  15020  vdwapun  15725  vdwlem1  15732  vdwlem12  15743  vdwlem13  15744  isacs2  16361  equivestrcsetc  16839  psgneu  17972  efglem  18175  lmisfree  20229  toprntopon  20777  neitr  21032  cmpsublem  21250  cmpsub  21251  bwth  21261  1stcfb  21296  unisngl  21378  alexsubALTlem3  21900  alexsubALTlem4  21901  vitali  23427  mbfi1fseqlem6  23532  mbfi1flimlem  23534  aannenlem2  24129  istrkg2ld  25404  axlowdim  25886  wlkpwwlkf1ouspgr  26833  wlkisowwlkupgr  26834  padct  29625  cnvoprabOLD  29626  f1ocnt  29687  locfinreflem  30035  locfinref  30036  prsdm  30088  prsrn  30089  eulerpart  30572  bnj150  31072  trpredpred  31852  nosupno  31974  nosupfv  31977  fnsingle  32151  finminlem  32437  filnetlem3  32500  cnndvlem2  32654  bj-restpw  33170  bj-rest0  33171  poimirlem2  33541  mblfinlem3  33578  mblfinlem4  33579  ismblfin  33580  itg2addnclem  33591  itg2addnc  33594  indexdom  33659  sdclem2  33668  fdc  33671  prtlem16  34473  dihglblem2aN  36899  eldioph2lem2  37641  dford3lem2  37911  aomclem7  37947  dfac11  37949  relintabex  38204  rclexi  38239  trclexi  38244  rtrclexi  38245  fnchoice  39502  ssnnf1octb  39696  fzisoeu  39828  stoweidlem28  40563  nnfoctbdjlem  40990  smfpimcclem  41334  setrec1lem3  42761  setrec2lem2  42766
  Copyright terms: Public domain W3C validator