Theorem spcev 3565

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570  ∃wex 1809   ∈ wcel 2143  Vcvv 3455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-clel 2838

This theorem is referenced by:  dtruALT  5359  nnullss  5443  exss  5444  euotd  5496  opeldm  5897  elrnmpt1  5950  xpnz  6156  ssimaex  6966  fvelrn  7071  dff3  7095  exfo  7100  eufnfv  7227  elunirn  7249  fsnex  7281  f1prex  7282  foeqcnvco  7298  ffoss  7939  op1steq  8026  frxp  8118  suppimacnv  8166  seqomlem2  8434  domtr  9000  en1  9017  enfixsn  9070  ssfiALT  9154  php3  9189  isinf  9221  ac6sfi  9240  hartogslem1  9500  brwdom2  9531  inf0  9586  axinf2  9605  cnfcom3clem  9670  ssttrcl  9680  ttrcltr  9681  ttrclss  9685  ttrclselem2  9691  tz9.1c  9695  rankuni  9831  scott0  9856  bnd2  9875  cardprclem  9961  dfac4  10102  dfac5lem5  10107  dfac5  10108  dfac2a  10109  dfac2b  10110  kmlem2  10131  kmlem13  10142  ackbij2  10221  cfsuc  10236  cfflb  10238  cfss  10244  cfsmolem  10249  cfcoflem  10251  fin23lem32  10323  axcc2lem  10415  axcc3  10417  axdc2lem  10427  axdc3lem2  10430  axcclem  10436  brdom3  10507  brdom7disj  10510  brdom6disj  10511  axpowndlem3  10579  canthnumlem  10628  canthp1lem2  10633  inar1  10755  recmulnq  10944  ltexnq  10955  halfnq  10956  ltbtwnnq  10958  1idpr  11009  ltexprlem7  11022  reclem2pr  11028  reclem3pr  11029  sup2  12166  nnunb  12495  uzrdgfni  13990  axdc4uzlem  14015  rtrclreclem3  15093  ntrivcvgmullem  15951  fprodntriv  15992  cnso  16298  vdwapun  17029  vdwlem1  17036  vdwlem12  17047  vdwlem13  17048  isacs2  17704  equivestrcsetc  18203  psgneu  19571  efglem  19781  lmisfree  21992  toprntopon  23082  neitr  23337  cmpsublem  23556  cmpsub  23557  bwth  23567  1stcfb  23602  unisngl  23684  alexsubALTlem3  24206  alexsubALTlem4  24207  vitali  25772  mbfi1fseqlem6  25879  mbfi1flimlem  25881  aannenlem2  26492  nosupno  27867  nosupfv  27870  noinfno  27882  noinffv  27885  noseqrdgfn  28499  istrkg2ld  28729  axlowdim  29311  wlkswwlksf1o  30228  clwlkclwwlkf  30359  padct  33063  f1ocnt  33145  cycpmconjslem2  33475  locfinreflem  34230  locfinref  34231  prsdm  34304  prsrn  34305  eulerpart  34772  fineqvac  35529  satf0op  35869  prv1n  35923  fnsingle  36409  finminlem  36829  filnetlem3  36891  dfttc4lem1  37039  regsfromregtco  37049  cnndvlem2  37127  bj-restpw  37734  bj-rest0  37735  exrecfnlem  38025  ctbssinf  38052  poimirlem2  38273  mblfinlem3  38310  mblfinlem4  38311  ismblfin  38312  itg2addnclem  38322  itg2addnc  38325  indexdom  38385  sdclem2  38393  fdc  38396  prtlem16  39643  dihglblem2aN  42067  sn-sup2  43265  eldioph2lem2  43492  dford3lem2  43754  aomclem7  43787  dfac11  43789  rclexi  44341  trclexi  44346  rtrclexi  44347  permaxinf2lem  45721  permac8prim  45723  fnchoice  45749  ssnnf1octb  45912  fzisoeu  46019  stoweidlem28  46742  nnfoctbdjlem  47169  smfpimcclem  47521  funressndmafv2rn  47960  mof0  49616  nelsubc3lem  49848  initc  49869  setc2othin  50244  cnelsubclem  50381  setrec1lem3  50467  setrec2lem2  50472