Theorem spcev 3452

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

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1652  ∃wex 1874   ∈ wcel 2155  Vcvv 3350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352

This theorem is referenced by:  dtruALT  5023  elALT  5066  dtruALT2  5067  nnullss  5086  exss  5087  euotd  5134  opeldm  5496  elrnmpt1  5543  xpnz  5736  ssimaex  6452  fvelrn  6542  dff3  6562  exfo  6567  eufnfv  6684  elunirn  6701  fsnex  6730  f1prex  6731  foeqcnvco  6747  snnexOLD  7165  ffoss  7325  op1steq  7410  frxp  7489  suppimacnv  7508  seqomlem2  7750  domtr  8213  ensn1  8224  en1  8227  enfixsn  8276  php3  8353  1sdom  8370  isinf  8380  ssfi  8387  ac6sfi  8411  hartogslem1  8654  brwdom2  8685  inf0  8733  axinf2  8752  cnfcom3clem  8817  tz9.1  8820  tz9.1c  8821  rankuni  8941  scott0  8964  cplem2  8968  bnd2  8971  cardprclem  9056  dfac4  9196  dfac5lem5  9201  dfac5  9202  dfac2a  9203  dfac2b  9204  dfac2OLD  9206  kmlem2  9226  kmlem13  9237  ackbij2  9318  cfsuc  9332  cfflb  9334  cfss  9340  cfsmolem  9345  cfcoflem  9347  fin23lem32  9419  axcc2lem  9511  axcc3  9513  axdc2lem  9523  axdc3lem2  9526  axcclem  9532  brdom3  9603  brdom7disj  9606  brdom6disj  9607  axpowndlem3  9674  canthnumlem  9723  canthp1lem2  9728  inar1  9850  recmulnq  10039  ltexnq  10050  halfnq  10051  ltbtwnnq  10053  1idpr  10104  ltexprlem7  10117  reclem2pr  10123  reclem3pr  10124  sup2  11233  nnunb  11534  uzrdgfni  12965  axdc4uzlem  12990  rtrclreclem3  14087  ntrivcvgmullem  14918  fprodntriv  14957  cnso  15260  vdwapun  15959  vdwlem1  15966  vdwlem12  15977  vdwlem13  15978  isacs2  16581  equivestrcsetc  17060  psgneu  18192  efglem  18395  lmisfree  20457  toprntopon  21009  neitr  21264  cmpsublem  21482  cmpsub  21483  bwth  21493  1stcfb  21528  unisngl  21610  alexsubALTlem3  22132  alexsubALTlem4  22133  vitali  23671  mbfi1fseqlem6  23778  mbfi1flimlem  23780  aannenlem2  24375  istrkg2ld  25650  axlowdim  26132  wlkswwlksf1o  27069  padct  29881  cnvoprabOLD  29882  f1ocnt  29943  locfinreflem  30289  locfinref  30290  prsdm  30342  prsrn  30343  eulerpart  30826  bnj150  31326  trpredpred  32103  nosupno  32225  nosupfv  32228  fnsingle  32402  finminlem  32688  filnetlem3  32750  cnndvlem2  32900  bj-restpw  33405  bj-rest0  33406  poimirlem2  33767  mblfinlem3  33804  mblfinlem4  33805  ismblfin  33806  itg2addnclem  33816  itg2addnc  33819  indexdom  33884  sdclem2  33892  fdc  33895  prtlem16  34757  dihglblem2aN  37181  eldioph2lem2  37934  dford3lem2  38203  aomclem7  38239  dfac11  38241  relintabex  38494  rclexi  38529  trclexi  38534  rtrclexi  38535  fnchoice  39772  ssnnf1octb  39961  fzisoeu  40085  stoweidlem28  40814  nnfoctbdjlem  41241  smfpimcclem  41585  funressndmafv2rn  41903  setrec1lem3  43037  setrec2lem2  43042