Theorem spcev 3525

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 3516	. 2 ⊢ (𝐴 ∈ V → (𝜓 → ∃𝑥𝜑))
4	1, 3	ax-mp 5	1 ⊢ (𝜓 → ∃𝑥𝜑)

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1507  ∃wex 1742   ∈ wcel 2050  Vcvv 3415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2771  df-clel 2846

This theorem is referenced by:  dtruALT  5141  sels  5190  elALT  5191  dtruALT2  5192  nnullss  5211  exss  5212  euotd  5259  opeldm  5626  elrnmpt1  5673  xpnz  5856  ssimaex  6576  fvelrn  6669  dff3  6689  exfo  6694  eufnfv  6817  elunirn  6835  fsnex  6864  f1prex  6865  foeqcnvco  6881  ffoss  7459  op1steq  7545  frxp  7625  suppimacnv  7644  seqomlem2  7890  domtr  8359  en1  8373  enfixsn  8422  php3  8499  1sdom  8516  isinf  8526  ssfi  8533  ac6sfi  8557  hartogslem1  8801  brwdom2  8832  inf0  8878  axinf2  8897  cnfcom3clem  8962  tz9.1c  8966  rankuni  9086  scott0  9109  bnd2  9116  cardprclem  9202  dfac4  9342  dfac5lem5  9347  dfac5  9348  dfac2a  9349  dfac2b  9350  kmlem2  9371  kmlem13  9382  ackbij2  9463  cfsuc  9477  cfflb  9479  cfss  9485  cfsmolem  9490  cfcoflem  9492  fin23lem32  9564  axcc2lem  9656  axcc3  9658  axdc2lem  9668  axdc3lem2  9671  axcclem  9677  brdom3  9748  brdom7disj  9751  brdom6disj  9752  axpowndlem3  9819  canthnumlem  9868  canthp1lem2  9873  inar1  9995  recmulnq  10184  ltexnq  10195  halfnq  10196  ltbtwnnq  10198  1idpr  10249  ltexprlem7  10262  reclem2pr  10268  reclem3pr  10269  sup2  11398  nnunb  11703  uzrdgfni  13141  axdc4uzlem  13166  rtrclreclem3  14280  ntrivcvgmullem  15117  fprodntriv  15156  cnso  15460  vdwapun  16166  vdwlem1  16173  vdwlem12  16184  vdwlem13  16185  isacs2  16782  equivestrcsetc  17260  psgneu  18396  efglem  18600  lmisfree  20688  toprntopon  21237  neitr  21492  cmpsublem  21711  cmpsub  21712  bwth  21722  1stcfb  21757  unisngl  21839  alexsubALTlem3  22361  alexsubALTlem4  22362  vitali  23917  mbfi1fseqlem6  24024  mbfi1flimlem  24026  aannenlem2  24621  istrkg2ld  25948  axlowdim  26450  wlkswwlksf1o  27365  clwlkclwwlkf  27522  padct  30214  cnvoprabOLD  30215  f1ocnt  30279  locfinreflem  30754  locfinref  30755  prsdm  30807  prsrn  30808  eulerpart  31291  satf0op  32193  trpredpred  32594  nosupno  32730  nosupfv  32733  fnsingle  32907  finminlem  33193  filnetlem3  33255  cnndvlem2  33403  bj-restpw  33899  bj-rest0  33900  exrecfnlem  34108  ctbssinf  34134  poimirlem2  34341  mblfinlem3  34378  mblfinlem4  34379  ismblfin  34380  itg2addnclem  34390  itg2addnc  34393  indexdom  34457  sdclem2  34465  fdc  34468  prtlem16  35456  dihglblem2aN  37880  eldioph2lem2  38759  dford3lem2  39026  aomclem7  39062  dfac11  39064  relintabex  39309  rclexi  39344  trclexi  39349  rtrclexi  39350  fnchoice  40711  ssnnf1octb  40886  fzisoeu  41002  stoweidlem28  41750  nnfoctbdjlem  42174  smfpimcclem  42518  funressndmafv2rn  42834  setrec1lem3  44165  setrec2lem2  44170