Theorem spcev 3609

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

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

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 2795

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

This theorem is referenced by:  dtruALT  5291  sels  5336  elALT  5337  dtruALT2  5338  nnullss  5356  exss  5357  euotd  5405  opeldm  5778  elrnmpt1  5832  xpnz  6018  ssimaex  6750  fvelrn  6846  dff3  6868  exfo  6873  eufnfv  6993  elunirn  7012  fsnex  7041  f1prex  7042  foeqcnvco  7058  ffoss  7649  op1steq  7735  frxp  7822  suppimacnv  7843  seqomlem2  8089  domtr  8564  en1  8578  enfixsn  8628  php3  8705  1sdom  8723  isinf  8733  ssfi  8740  ac6sfi  8764  hartogslem1  9008  brwdom2  9039  inf0  9086  axinf2  9105  cnfcom3clem  9170  tz9.1c  9174  rankuni  9294  scott0  9317  bnd2  9324  cardprclem  9410  dfac4  9550  dfac5lem5  9555  dfac5  9556  dfac2a  9557  dfac2b  9558  kmlem2  9579  kmlem13  9590  ackbij2  9667  cfsuc  9681  cfflb  9683  cfss  9689  cfsmolem  9694  cfcoflem  9696  fin23lem32  9768  axcc2lem  9860  axcc3  9862  axdc2lem  9872  axdc3lem2  9875  axcclem  9881  brdom3  9952  brdom7disj  9955  brdom6disj  9956  axpowndlem3  10023  canthnumlem  10072  canthp1lem2  10077  inar1  10199  recmulnq  10388  ltexnq  10399  halfnq  10400  ltbtwnnq  10402  1idpr  10453  ltexprlem7  10466  reclem2pr  10472  reclem3pr  10473  sup2  11599  nnunb  11896  uzrdgfni  13329  axdc4uzlem  13354  rtrclreclem3  14421  ntrivcvgmullem  15259  fprodntriv  15298  cnso  15602  vdwapun  16312  vdwlem1  16319  vdwlem12  16330  vdwlem13  16331  isacs2  16926  equivestrcsetc  17404  psgneu  18636  efglem  18844  lmisfree  20988  toprntopon  21535  neitr  21790  cmpsublem  22009  cmpsub  22010  bwth  22020  1stcfb  22055  unisngl  22137  alexsubALTlem3  22659  alexsubALTlem4  22660  vitali  24216  mbfi1fseqlem6  24323  mbfi1flimlem  24325  aannenlem2  24920  istrkg2ld  26248  axlowdim  26749  wlkswwlksf1o  27659  clwlkclwwlkf  27788  padct  30457  cnvoprabOLD  30458  f1ocnt  30527  cycpmconjslem2  30799  locfinreflem  31106  locfinref  31107  prsdm  31159  prsrn  31160  eulerpart  31642  satf0op  32626  prv1n  32680  trpredpred  33069  nosupno  33205  nosupfv  33208  fnsingle  33382  finminlem  33668  filnetlem3  33730  cnndvlem2  33879  bj-restpw  34385  bj-rest0  34386  exrecfnlem  34662  ctbssinf  34689  poimirlem2  34896  mblfinlem3  34933  mblfinlem4  34934  ismblfin  34935  itg2addnclem  34945  itg2addnc  34948  indexdom  35011  sdclem2  35019  fdc  35022  prtlem16  36007  dihglblem2aN  38431  eldioph2lem2  39365  dford3lem2  39631  aomclem7  39667  dfac11  39669  rclexi  39982  trclexi  39987  rtrclexi  39988  fnchoice  41293  ssnnf1octb  41463  fzisoeu  41574  stoweidlem28  42320  nnfoctbdjlem  42744  smfpimcclem  43088  funressndmafv2rn  43429  setrec1lem3  44799  setrec2lem2  44804