Theorem spcev 3575

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∃wex 1779   ∈ wcel 2109  Vcvv 3450

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-clel 2804

This theorem is referenced by:  dtruALT  5346  nnullss  5425  exss  5426  euotd  5476  opeldm  5874  elrnmpt1  5927  xpnz  6135  ssimaex  6949  fvelrn  7051  dff3  7075  exfo  7080  eufnfv  7206  elunirn  7228  fsnex  7261  f1prex  7262  foeqcnvco  7278  ffoss  7927  op1steq  8015  frxp  8108  suppimacnv  8156  seqomlem2  8422  domtr  8981  en1  8998  enfixsn  9055  ssfiALT  9144  php3  9179  1sdomOLD  9203  isinf  9214  isinfOLD  9215  ac6sfi  9238  hartogslem1  9502  brwdom2  9533  inf0  9581  axinf2  9600  cnfcom3clem  9665  ssttrcl  9675  ttrcltr  9676  ttrclss  9680  ttrclselem2  9686  tz9.1c  9690  rankuni  9823  scott0  9846  bnd2  9853  cardprclem  9939  dfac4  10082  dfac5lem5  10087  dfac5  10089  dfac2a  10090  dfac2b  10091  kmlem2  10112  kmlem13  10123  ackbij2  10202  cfsuc  10217  cfflb  10219  cfss  10225  cfsmolem  10230  cfcoflem  10232  fin23lem32  10304  axcc2lem  10396  axcc3  10398  axdc2lem  10408  axdc3lem2  10411  axcclem  10417  brdom3  10488  brdom7disj  10491  brdom6disj  10492  axpowndlem3  10559  canthnumlem  10608  canthp1lem2  10613  inar1  10735  recmulnq  10924  ltexnq  10935  halfnq  10936  ltbtwnnq  10938  1idpr  10989  ltexprlem7  11002  reclem2pr  11008  reclem3pr  11009  sup2  12146  nnunb  12445  uzrdgfni  13930  axdc4uzlem  13955  rtrclreclem3  15033  ntrivcvgmullem  15874  fprodntriv  15915  cnso  16222  vdwapun  16952  vdwlem1  16959  vdwlem12  16970  vdwlem13  16971  isacs2  17621  equivestrcsetc  18120  psgneu  19443  efglem  19653  lmisfree  21758  toprntopon  22819  neitr  23074  cmpsublem  23293  cmpsub  23294  bwth  23304  1stcfb  23339  unisngl  23421  alexsubALTlem3  23943  alexsubALTlem4  23944  vitali  25521  mbfi1fseqlem6  25628  mbfi1flimlem  25630  aannenlem2  26244  nosupno  27622  nosupfv  27625  noinfno  27637  noinffv  27640  noseqrdgfn  28207  istrkg2ld  28394  axlowdim  28895  wlkswwlksf1o  29816  clwlkclwwlkf  29944  padct  32650  f1ocnt  32732  cycpmconjslem2  33119  locfinreflem  33837  locfinref  33838  prsdm  33911  prsrn  33912  eulerpart  34380  fineqvac  35094  satf0op  35371  prv1n  35425  fnsingle  35914  finminlem  36313  filnetlem3  36375  cnndvlem2  36533  bj-restpw  37087  bj-rest0  37088  exrecfnlem  37374  ctbssinf  37401  poimirlem2  37623  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  itg2addnclem  37672  itg2addnc  37675  indexdom  37735  sdclem2  37743  fdc  37746  prtlem16  38869  dihglblem2aN  41294  sn-sup2  42486  eldioph2lem2  42756  dford3lem2  43023  aomclem7  43056  dfac11  43058  rclexi  43611  trclexi  43616  rtrclexi  43617  permaxinf2lem  45009  permac8prim  45011  fnchoice  45030  ssnnf1octb  45195  fzisoeu  45305  stoweidlem28  46033  nnfoctbdjlem  46460  smfpimcclem  46812  funressndmafv2rn  47228  mof0  48830  nelsubc3lem  49063  initc  49084  setc2othin  49459  cnelsubclem  49596  setrec1lem3  49682  setrec2lem2  49687