Theorem spcev 3564

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ∃wex 1812   ∈ wcel 2147  Vcvv 3454

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-clel 2839

This theorem is used by:  dtruALT  5357  nnullss  5437  exss  5438  euotd  5493  opeldm  5901  elrnmpt1  5954  xpnz  6168  ssimaex  7001  fvelrn  7108  dff3  7132  exfo  7137  eufnfv  7266  elunirn  7286  fsnex  7322  f1prex  7323  foeqcnvco  7339  ffoss  7992  op1steq  8079  frxp  8175  suppimacnv  8229  seqomlem2  8499  domtr  9072  en1  9089  enfixsn  9143  ssfiALT  9227  php3  9262  isinf  9294  ac6sfi  9313  hartogslem1  9573  brwdom2  9604  inf0  9659  axinf2  9678  cnfcom3clem  9743  ssttrcl  9753  ttrcltr  9754  ttrclss  9758  ttrclselem2  9764  tz9.1c  9768  rankuni  9916  scott0b  9974  scott0OLD  9975  bnd2  9993  setrec1lem3  10006  setrec2lem2  10013  cardprclem  10097  dfac4  10240  dfac5lem5  10245  dfac5  10246  dfac2a  10247  dfac2b  10248  kmlem2  10269  kmlem13  10280  ackbij2  10359  cfsuc  10374  cfflb  10376  cfss  10382  cfsmolem  10387  cfcoflem  10389  fin23lem32  10461  axcc2lem  10553  axcc3  10555  axdc2lem  10565  axdc3lem2  10568  axcclem  10574  brdom3  10646  brdom7disj  10649  brdom6disj  10650  axpowndlem3  10723  canthnumlem  10772  canthp1lem2  10777  inar1  10899  recmulnq  11088  ltexnq  11099  halfnq  11100  ltbtwnnq  11102  1idpr  11153  ltexprlem7  11166  reclem2pr  11172  reclem3pr  11173  sup2  12313  nnunb  12642  uzrdgfni  14141  axdc4uzlem  14166  rtrclreclem3  15256  ntrivcvgmullem  16114  fprodntriv  16153  cnso  16459  vdwapun  17196  vdwlem1  17203  vdwlem12  17214  vdwlem13  17215  isacs2  17877  equivestrcsetc  18376  psgneu  19771  efglem  19981  lmisfree  22203  toprntopon  23298  neitr  23553  cmpsublem  23772  cmpsub  23773  bwth  23783  1stcfb  23818  unisngl  23901  alexsubALTlem3  24423  alexsubALTlem4  24424  vitali  25989  mbfi1fseqlem6  26096  mbfi1flimlem  26098  aannenlem2  26713  nosupno  28117  nosupfv  28120  noinfno  28132  noinffv  28135  noseqrdgfn  28749  istrkg2ld  28979  axlowdim  29596  wlkswwlksf1o  30525  clwlkclwwlkf  30656  padct  33407  f1ocnt  33488  cycpmconjslem2  33815  locfinreflem  34583  locfinref  34584  prsdm  34657  prsrn  34658  eulerpart  35125  dfac15  35886  weexenwe  35889  fineqvac  35925  vonf1onprcf1ac  36085  onprcf1acwevdlem1  36086  satf0op  36350  prv1n  36404  elpssex  36672  fnsingle  36896  finminlem  37321  filnetlem3  37383  dfttc4lem1  37531  regsfromregtco  37541  cnndvlem2  37619  bj-restpw  38283  bj-rest0  38284  exrecfnlem  38570  ctbssinf  38597  poimirlem2  38808  mblfinlem3  38845  mblfinlem4  38846  ismblfin  38847  itg2addnclem  38857  itg2addnc  38860  indexdom  38936  sdclem2  38942  fdc  38945  prtlem16  40192  dihglblem2aN  42616  sn-sup2  43821  eldioph2lem2  44038  dford3lem2  44300  aomclem7  44328  dfac11  44330  rclexi  44876  trclexi  44881  rtrclexi  44882  permaxinf2lem  46266  permac8prim  46268  fnchoice  46320  ssnnf1octb  46482  fzisoeu  46589  stoweidlem28  47311  nnfoctbdjlem  47738  smfpimcclem  48090  funressndmafv2rn  48566  mof0  50280  nelsubc3lem  50515  initc  50537  setc2othin  50932  cnelsubcw  51072