Theorem spcev 3550

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ∃wex 1779   ∈ wcel 2104  Vcvv 3437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-clel 2814

This theorem is referenced by:  dtruALT  5320  sels  5369  elALT  5371  nnullss  5390  exss  5391  euotd  5440  opeldm  5829  elrnmpt1  5879  xpnz  6077  ssimaex  6885  fvelrn  6986  dff3  7008  exfo  7013  eufnfv  7137  elunirn  7156  fsnex  7187  f1prex  7188  foeqcnvco  7204  ffoss  7820  op1steq  7907  frxp  7998  suppimacnv  8021  seqomlem2  8313  domtr  8828  en1  8846  en1OLD  8847  enfixsn  8906  ssfiALT  8995  php3  9033  php3OLD  9045  1sdomOLD  9070  isinf  9080  ac6sfi  9102  hartogslem1  9345  brwdom2  9376  inf0  9423  axinf2  9442  cnfcom3clem  9507  ssttrcl  9517  ttrcltr  9518  ttrclss  9522  ttrclselem2  9528  tz9.1c  9532  rankuni  9665  scott0  9688  bnd2  9695  cardprclem  9781  dfac4  9924  dfac5lem5  9929  dfac5  9930  dfac2a  9931  dfac2b  9932  kmlem2  9953  kmlem13  9964  ackbij2  10045  cfsuc  10059  cfflb  10061  cfss  10067  cfsmolem  10072  cfcoflem  10074  fin23lem32  10146  axcc2lem  10238  axcc3  10240  axdc2lem  10250  axdc3lem2  10253  axcclem  10259  brdom3  10330  brdom7disj  10333  brdom6disj  10334  axpowndlem3  10401  canthnumlem  10450  canthp1lem2  10455  inar1  10577  recmulnq  10766  ltexnq  10777  halfnq  10778  ltbtwnnq  10780  1idpr  10831  ltexprlem7  10844  reclem2pr  10850  reclem3pr  10851  sup2  11977  nnunb  12275  uzrdgfni  13724  axdc4uzlem  13749  rtrclreclem3  14816  ntrivcvgmullem  15658  fprodntriv  15697  cnso  16001  vdwapun  16720  vdwlem1  16727  vdwlem12  16738  vdwlem13  16739  isacs2  17407  equivestrcsetc  17914  psgneu  19159  efglem  19367  lmisfree  21094  toprntopon  22119  neitr  22376  cmpsublem  22595  cmpsub  22596  bwth  22606  1stcfb  22641  unisngl  22723  alexsubALTlem3  23245  alexsubALTlem4  23246  vitali  24822  mbfi1fseqlem6  24930  mbfi1flimlem  24932  aannenlem2  25534  istrkg2ld  26866  axlowdim  27374  wlkswwlksf1o  28289  clwlkclwwlkf  28417  padct  31099  cnvoprabOLD  31100  f1ocnt  31168  cycpmconjslem2  31467  locfinreflem  31835  locfinref  31836  prsdm  31909  prsrn  31910  eulerpart  32394  fineqvac  33111  satf0op  33384  prv1n  33438  nosupno  33951  nosupfv  33954  noinfno  33966  noinffv  33969  fnsingle  34266  finminlem  34552  filnetlem3  34614  cnndvlem2  34763  bj-restpw  35307  bj-rest0  35308  exrecfnlem  35594  ctbssinf  35621  poimirlem2  35823  mblfinlem3  35860  mblfinlem4  35861  ismblfin  35862  itg2addnclem  35872  itg2addnc  35875  indexdom  35936  sdclem2  35944  fdc  35947  prtlem16  36925  dihglblem2aN  39349  sn-sup2  40476  eldioph2lem2  40620  dford3lem2  40887  aomclem7  40923  dfac11  40925  rclexi  41261  trclexi  41266  rtrclexi  41267  fnchoice  42610  ssnnf1octb  42777  fzisoeu  42887  stoweidlem28  43618  nnfoctbdjlem  44043  smfpimcclem  44394  funressndmafv2rn  44773  mof0  46223  setc2othin  46395  setrec1lem3  46453  setrec2lem2  46458