Theorem spcev 3558

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ∃wex 1780   ∈ wcel 2113  Vcvv 3438

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 1968  ax-7 2009  ax-8 2115

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-clel 2809

This theorem is referenced by:  dtruALT  5331  nnullss  5408  exss  5409  euotd  5459  opeldm  5854  elrnmpt1  5907  xpnz  6115  ssimaex  6917  fvelrn  7019  dff3  7043  exfo  7048  eufnfv  7173  elunirn  7195  fsnex  7227  f1prex  7228  foeqcnvco  7244  ffoss  7888  op1steq  7975  frxp  8066  suppimacnv  8114  seqomlem2  8380  domtr  8942  en1  8959  enfixsn  9012  ssfiALT  9096  php3  9131  isinf  9163  ac6sfi  9182  hartogslem1  9445  brwdom2  9476  inf0  9528  axinf2  9547  cnfcom3clem  9612  ssttrcl  9622  ttrcltr  9623  ttrclss  9627  ttrclselem2  9633  tz9.1c  9637  rankuni  9773  scott0  9796  bnd2  9803  cardprclem  9889  dfac4  10030  dfac5lem5  10035  dfac5  10037  dfac2a  10038  dfac2b  10039  kmlem2  10060  kmlem13  10071  ackbij2  10150  cfsuc  10165  cfflb  10167  cfss  10173  cfsmolem  10178  cfcoflem  10180  fin23lem32  10252  axcc2lem  10344  axcc3  10346  axdc2lem  10356  axdc3lem2  10359  axcclem  10365  brdom3  10436  brdom7disj  10439  brdom6disj  10440  axpowndlem3  10508  canthnumlem  10557  canthp1lem2  10562  inar1  10684  recmulnq  10873  ltexnq  10884  halfnq  10885  ltbtwnnq  10887  1idpr  10938  ltexprlem7  10951  reclem2pr  10957  reclem3pr  10958  sup2  12096  nnunb  12395  uzrdgfni  13879  axdc4uzlem  13904  rtrclreclem3  14981  ntrivcvgmullem  15822  fprodntriv  15863  cnso  16170  vdwapun  16900  vdwlem1  16907  vdwlem12  16918  vdwlem13  16919  isacs2  17574  equivestrcsetc  18073  psgneu  19433  efglem  19643  lmisfree  21795  toprntopon  22867  neitr  23122  cmpsublem  23341  cmpsub  23342  bwth  23352  1stcfb  23387  unisngl  23469  alexsubALTlem3  23991  alexsubALTlem4  23992  vitali  25568  mbfi1fseqlem6  25675  mbfi1flimlem  25677  aannenlem2  26291  nosupno  27669  nosupfv  27672  noinfno  27684  noinffv  27687  noseqrdgfn  28267  istrkg2ld  28481  axlowdim  28983  wlkswwlksf1o  29901  clwlkclwwlkf  30032  padct  32746  f1ocnt  32829  cycpmconjslem2  33186  locfinreflem  33946  locfinref  33947  prsdm  34020  prsrn  34021  eulerpart  34488  fineqvac  35221  satf0op  35520  prv1n  35574  fnsingle  36060  finminlem  36461  filnetlem3  36523  cnndvlem2  36681  bj-restpw  37236  bj-rest0  37237  exrecfnlem  37523  ctbssinf  37550  poimirlem2  37762  mblfinlem3  37799  mblfinlem4  37800  ismblfin  37801  itg2addnclem  37811  itg2addnc  37814  indexdom  37874  sdclem2  37882  fdc  37885  prtlem16  39068  dihglblem2aN  41492  sn-sup2  42688  eldioph2lem2  42945  dford3lem2  43211  aomclem7  43244  dfac11  43246  rclexi  43798  trclexi  43803  rtrclexi  43804  permaxinf2lem  45195  permac8prim  45197  fnchoice  45216  ssnnf1octb  45380  fzisoeu  45490  stoweidlem28  46214  nnfoctbdjlem  46641  smfpimcclem  46993  funressndmafv2rn  47411  mof0  49025  nelsubc3lem  49257  initc  49278  setc2othin  49653  cnelsubclem  49790  setrec1lem3  49876  setrec2lem2  49881