Theorem spcev 3560

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-clel 2835

This theorem is used by:  dtruALT  5353  nnullss  5437  exss  5438  euotd  5490  opeldm  5891  elrnmpt1  5944  xpnz  6151  ssimaex  6963  fvelrn  7069  dff3  7093  exfo  7098  eufnfv  7228  elunirn  7248  fsnex  7284  f1prex  7285  foeqcnvco  7301  ffoss  7943  op1steq  8030  frxp  8124  suppimacnv  8172  seqomlem2  8440  domtr  9013  en1  9030  enfixsn  9084  ssfiALT  9168  php3  9203  isinf  9235  ac6sfi  9254  hartogslem1  9514  brwdom2  9545  inf0  9600  axinf2  9619  cnfcom3clem  9684  ssttrcl  9694  ttrcltr  9695  ttrclss  9699  ttrclselem2  9705  tz9.1c  9709  rankuni  9845  scott0b  9876  scott0OLD  9877  bnd2  9895  cardprclem  9984  dfac4  10125  dfac5lem5  10130  dfac5  10131  dfac2a  10132  dfac2b  10133  kmlem2  10154  kmlem13  10165  ackbij2  10244  cfsuc  10259  cfflb  10261  cfss  10267  cfsmolem  10272  cfcoflem  10274  fin23lem32  10346  axcc2lem  10438  axcc3  10440  axdc2lem  10450  axdc3lem2  10453  axcclem  10459  brdom3  10531  brdom7disj  10534  brdom6disj  10535  axpowndlem3  10608  canthnumlem  10657  canthp1lem2  10662  inar1  10784  recmulnq  10973  ltexnq  10984  halfnq  10985  ltbtwnnq  10987  1idpr  11038  ltexprlem7  11051  reclem2pr  11057  reclem3pr  11058  sup2  12195  nnunb  12524  uzrdgfni  14022  axdc4uzlem  14047  rtrclreclem3  15133  ntrivcvgmullem  15990  fprodntriv  16029  cnso  16335  vdwapun  17066  vdwlem1  17073  vdwlem12  17084  vdwlem13  17085  isacs2  17741  equivestrcsetc  18240  psgneu  19633  efglem  19843  lmisfree  22055  toprntopon  23150  neitr  23405  cmpsublem  23624  cmpsub  23625  bwth  23635  1stcfb  23670  unisngl  23753  alexsubALTlem3  24275  alexsubALTlem4  24276  vitali  25841  mbfi1fseqlem6  25948  mbfi1flimlem  25950  aannenlem2  26565  nosupno  27939  nosupfv  27942  noinfno  27954  noinffv  27957  noseqrdgfn  28571  istrkg2ld  28801  axlowdim  29418  wlkswwlksf1o  30347  clwlkclwwlkf  30478  padct  33189  f1ocnt  33271  cycpmconjslem2  33595  locfinreflem  34350  locfinref  34351  prsdm  34424  prsrn  34425  eulerpart  34893  fineqvac  35642  satf0op  35956  prv1n  36010  fnsingle  36496  finminlem  36937  filnetlem3  36999  dfttc4lem1  37147  regsfromregtco  37157  cnndvlem2  37235  bj-restpw  37842  bj-rest0  37843  exrecfnlem  38133  ctbssinf  38160  poimirlem2  38371  mblfinlem3  38408  mblfinlem4  38409  ismblfin  38410  itg2addnclem  38420  itg2addnc  38423  indexdom  38484  sdclem2  38492  fdc  38495  prtlem16  39742  dihglblem2aN  42166  sn-sup2  43379  eldioph2lem2  43606  dford3lem2  43868  aomclem7  43901  dfac11  43903  rclexi  44455  trclexi  44460  rtrclexi  44461  permaxinf2lem  45835  permac8prim  45837  fnchoice  45863  ssnnf1octb  46026  fzisoeu  46133  stoweidlem28  46856  nnfoctbdjlem  47283  smfpimcclem  47635  funressndmafv2rn  48111  mof0  49766  nelsubc3lem  49996  initc  50017  setc2othin  50392  cnelsubclem  50529  setrec1lem3  50615  setrec2lem2  50620