Theorem spcev 3562

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-clel 2812

This theorem is referenced by:  dtruALT  5335  nnullss  5417  exss  5418  euotd  5469  opeldm  5864  elrnmpt1  5917  xpnz  6125  ssimaex  6927  fvelrn  7030  dff3  7054  exfo  7059  eufnfv  7185  elunirn  7207  fsnex  7239  f1prex  7240  foeqcnvco  7256  ffoss  7900  op1steq  7987  frxp  8078  suppimacnv  8126  seqomlem2  8392  domtr  8956  en1  8973  enfixsn  9026  ssfiALT  9110  php3  9145  isinf  9177  ac6sfi  9196  hartogslem1  9459  brwdom2  9490  inf0  9542  axinf2  9561  cnfcom3clem  9626  ssttrcl  9636  ttrcltr  9637  ttrclss  9641  ttrclselem2  9647  tz9.1c  9651  rankuni  9787  scott0  9810  bnd2  9817  cardprclem  9903  dfac4  10044  dfac5lem5  10049  dfac5  10051  dfac2a  10052  dfac2b  10053  kmlem2  10074  kmlem13  10085  ackbij2  10164  cfsuc  10179  cfflb  10181  cfss  10187  cfsmolem  10192  cfcoflem  10194  fin23lem32  10266  axcc2lem  10358  axcc3  10360  axdc2lem  10370  axdc3lem2  10373  axcclem  10379  brdom3  10450  brdom7disj  10453  brdom6disj  10454  axpowndlem3  10522  canthnumlem  10571  canthp1lem2  10576  inar1  10698  recmulnq  10887  ltexnq  10898  halfnq  10899  ltbtwnnq  10901  1idpr  10952  ltexprlem7  10965  reclem2pr  10971  reclem3pr  10972  sup2  12110  nnunb  12409  uzrdgfni  13893  axdc4uzlem  13918  rtrclreclem3  14995  ntrivcvgmullem  15836  fprodntriv  15877  cnso  16184  vdwapun  16914  vdwlem1  16921  vdwlem12  16932  vdwlem13  16933  isacs2  17588  equivestrcsetc  18087  psgneu  19447  efglem  19657  lmisfree  21809  toprntopon  22881  neitr  23136  cmpsublem  23355  cmpsub  23356  bwth  23366  1stcfb  23401  unisngl  23483  alexsubALTlem3  24005  alexsubALTlem4  24006  vitali  25582  mbfi1fseqlem6  25689  mbfi1flimlem  25691  aannenlem2  26305  nosupno  27683  nosupfv  27686  noinfno  27698  noinffv  27701  noseqrdgfn  28314  istrkg2ld  28544  axlowdim  29046  wlkswwlksf1o  29964  clwlkclwwlkf  30095  padct  32808  f1ocnt  32891  cycpmconjslem2  33249  locfinreflem  34018  locfinref  34019  prsdm  34092  prsrn  34093  eulerpart  34560  fineqvac  35294  satf0op  35593  prv1n  35647  fnsingle  36133  finminlem  36534  filnetlem3  36596  regsfromregtr  36690  cnndvlem2  36760  bj-restpw  37345  bj-rest0  37346  exrecfnlem  37634  ctbssinf  37661  poimirlem2  37873  mblfinlem3  37910  mblfinlem4  37911  ismblfin  37912  itg2addnclem  37922  itg2addnc  37925  indexdom  37985  sdclem2  37993  fdc  37996  prtlem16  39245  dihglblem2aN  41669  sn-sup2  42861  eldioph2lem2  43118  dford3lem2  43384  aomclem7  43417  dfac11  43419  rclexi  43971  trclexi  43976  rtrclexi  43977  permaxinf2lem  45368  permac8prim  45370  fnchoice  45389  ssnnf1octb  45553  fzisoeu  45662  stoweidlem28  46386  nnfoctbdjlem  46813  smfpimcclem  47165  funressndmafv2rn  47583  mof0  49197  nelsubc3lem  49429  initc  49450  setc2othin  49825  cnelsubclem  49962  setrec1lem3  50048  setrec2lem2  50053