Theorem spcev 3607

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  ∃wex 1780   ∈ wcel 2114  Vcvv 3494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893

This theorem is referenced by:  dtruALT  5289  sels  5334  elALT  5335  dtruALT2  5336  nnullss  5354  exss  5355  euotd  5403  opeldm  5776  elrnmpt1  5830  xpnz  6016  ssimaex  6748  fvelrn  6844  dff3  6866  exfo  6871  eufnfv  6991  elunirn  7010  fsnex  7039  f1prex  7040  foeqcnvco  7056  ffoss  7647  op1steq  7733  frxp  7820  suppimacnv  7841  seqomlem2  8087  domtr  8562  en1  8576  enfixsn  8626  php3  8703  1sdom  8721  isinf  8731  ssfi  8738  ac6sfi  8762  hartogslem1  9006  brwdom2  9037  inf0  9084  axinf2  9103  cnfcom3clem  9168  tz9.1c  9172  rankuni  9292  scott0  9315  bnd2  9322  cardprclem  9408  dfac4  9548  dfac5lem5  9553  dfac5  9554  dfac2a  9555  dfac2b  9556  kmlem2  9577  kmlem13  9588  ackbij2  9665  cfsuc  9679  cfflb  9681  cfss  9687  cfsmolem  9692  cfcoflem  9694  fin23lem32  9766  axcc2lem  9858  axcc3  9860  axdc2lem  9870  axdc3lem2  9873  axcclem  9879  brdom3  9950  brdom7disj  9953  brdom6disj  9954  axpowndlem3  10021  canthnumlem  10070  canthp1lem2  10075  inar1  10197  recmulnq  10386  ltexnq  10397  halfnq  10398  ltbtwnnq  10400  1idpr  10451  ltexprlem7  10464  reclem2pr  10470  reclem3pr  10471  sup2  11597  nnunb  11894  uzrdgfni  13327  axdc4uzlem  13352  rtrclreclem3  14419  ntrivcvgmullem  15257  fprodntriv  15296  cnso  15600  vdwapun  16310  vdwlem1  16317  vdwlem12  16328  vdwlem13  16329  isacs2  16924  equivestrcsetc  17402  psgneu  18634  efglem  18842  lmisfree  20986  toprntopon  21533  neitr  21788  cmpsublem  22007  cmpsub  22008  bwth  22018  1stcfb  22053  unisngl  22135  alexsubALTlem3  22657  alexsubALTlem4  22658  vitali  24214  mbfi1fseqlem6  24321  mbfi1flimlem  24323  aannenlem2  24918  istrkg2ld  26246  axlowdim  26747  wlkswwlksf1o  27657  clwlkclwwlkf  27786  padct  30455  cnvoprabOLD  30456  f1ocnt  30525  cycpmconjslem2  30797  locfinreflem  31104  locfinref  31105  prsdm  31157  prsrn  31158  eulerpart  31640  satf0op  32624  prv1n  32678  trpredpred  33067  nosupno  33203  nosupfv  33206  fnsingle  33380  finminlem  33666  filnetlem3  33728  cnndvlem2  33877  bj-restpw  34386  bj-rest0  34387  exrecfnlem  34663  ctbssinf  34690  poimirlem2  34909  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  itg2addnclem  34958  itg2addnc  34961  indexdom  35024  sdclem2  35032  fdc  35035  prtlem16  36020  dihglblem2aN  38444  eldioph2lem2  39407  dford3lem2  39673  aomclem7  39709  dfac11  39711  rclexi  40024  trclexi  40029  rtrclexi  40030  fnchoice  41335  ssnnf1octb  41505  fzisoeu  41616  stoweidlem28  42362  nnfoctbdjlem  42786  smfpimcclem  43130  funressndmafv2rn  43471  setrec1lem3  44841  setrec2lem2  44846