Theorem spcev 3273

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

Step	Hyp	Ref	Expression
1		spcv.1	. 2 ⊢ 𝐴 ∈ V
2		spcv.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	spcegv 3267	. 2 ⊢ (𝐴 ∈ V → (𝜓 → ∃𝑥𝜑))
4	1, 3	ax-mp 5	1 ⊢ (𝜓 → ∃𝑥𝜑)

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  ∃wex 1695   ∈ wcel 1977  Vcvv 3173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175

This theorem is referenced by:  dtruALT  4826  elALT  4837  dtruALT2  4838  nnullss  4857  exss  4858  euotd  4900  opeldm  5250  elrnmpt1  5295  xpnz  5472  ssimaex  6173  fvelrn  6260  dff3  6280  exfo  6285  eufnfv  6395  elunirn  6413  fsnex  6438  f1prex  6439  foeqcnvco  6455  snnex  6862  ffoss  7020  op1steq  7101  frxp  7174  suppimacnv  7193  seqomlem2  7433  domtr  7895  ensn1  7906  en1  7909  enfixsn  7954  php3  8031  1sdom  8048  isinf  8058  ssfi  8065  ac6sfi  8089  hartogslem1  8330  brwdom2  8361  inf0  8401  axinf2  8420  cnfcom3clem  8485  tz9.1  8488  tz9.1c  8489  rankuni  8609  scott0  8632  cplem2  8636  bnd2  8639  karden  8641  cardprclem  8688  dfac4  8828  dfac5lem5  8833  dfac5  8834  dfac2a  8835  dfac2  8836  kmlem2  8856  kmlem13  8867  ackbij2  8948  cfsuc  8962  cfflb  8964  cfss  8970  cfsmolem  8975  cfcoflem  8977  fin23lem32  9049  axcc2lem  9141  axcc3  9143  axdc2lem  9153  axdc3lem2  9156  axcclem  9162  brdom3  9231  brdom7disj  9234  brdom6disj  9235  axpowndlem3  9300  canthnumlem  9349  canthp1lem2  9354  inar1  9476  recmulnq  9665  ltexnq  9676  halfnq  9677  ltbtwnnq  9679  1idpr  9730  ltexprlem7  9743  reclem2pr  9749  reclem3pr  9750  sup2  10858  nnunb  11165  uzrdgfni  12619  axdc4uzlem  12644  rtrclreclem3  13648  ntrivcvgmullem  14472  fprodntriv  14511  cnso  14815  vdwapun  15516  vdwlem1  15523  vdwlem12  15534  vdwlem13  15535  isacs2  16137  equivestrcsetc  16615  psgneu  17749  efglem  17952  lmisfree  20000  neitr  20794  cmpsublem  21012  cmpsub  21013  bwth  21023  1stcfb  21058  unisngl  21140  alexsubALTlem3  21663  alexsubALTlem4  21664  vitali  23188  mbfi1fseqlem6  23293  mbfi1flimlem  23295  aannenlem2  23888  istrkg2ld  25159  axlowdim  25641  padct  28885  cnvoprab  28886  f1ocnt  28946  locfinreflem  29235  locfinref  29236  prsdm  29288  prsrn  29289  eulerpart  29771  bnj150  30200  trpredpred  30972  fnsingle  31196  finminlem  31482  filnetlem3  31545  cnndvlem2  31699  bj-restpw  32226  bj-rest0  32227  bj-toprntopon  32244  poimirlem2  32581  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  itg2addnclem  32631  itg2addnc  32634  indexdom  32699  sdclem2  32708  fdc  32711  prtlem16  33172  dihglblem2aN  35600  eldioph2lem2  36342  dford3lem2  36612  aomclem7  36648  dfac11  36650  relintabex  36906  rclexi  36941  trclexi  36946  rtrclexi  36947  fnchoice  38211  ssnnf1octb  38377  fzisoeu  38455  stoweidlem28  38921  nnfoctbdjlem  39348  1wlkpwwlkf1ouspgr  41076  1wlkisowwlkupgr  41077  setrec1lem3  42235  setrec2lem2  42240