Theorem spcev 3544

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  ∃wex 1786   ∈ wcel 2119  Vcvv 3431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-clel 2814

This theorem is referenced by:  dtruALT  5317  nnullss  5401  exss  5402  euotd  5454  opeldm  5849  elrnmpt1  5902  xpnz  6110  ssimaex  6912  fvelrn  7017  dff3  7041  exfo  7046  eufnfv  7173  elunirn  7195  fsnex  7227  f1prex  7228  foeqcnvco  7244  ffoss  7888  op1steq  7975  frxp  8066  suppimacnv  8114  seqomlem2  8380  domtr  8944  en1  8961  enfixsn  9014  ssfiALT  9098  php3  9133  isinf  9165  ac6sfi  9184  hartogslem1  9447  brwdom2  9478  inf0  9533  axinf2  9552  cnfcom3clem  9617  ssttrcl  9627  ttrcltr  9628  ttrclss  9632  ttrclselem2  9638  tz9.1c  9642  rankuni  9778  scott0  9801  bnd2  9808  cardprclem  9894  dfac4  10035  dfac5lem5  10040  dfac5  10042  dfac2a  10043  dfac2b  10044  kmlem2  10065  kmlem13  10076  ackbij2  10155  cfsuc  10170  cfflb  10172  cfss  10178  cfsmolem  10183  cfcoflem  10185  fin23lem32  10257  axcc2lem  10349  axcc3  10351  axdc2lem  10361  axdc3lem2  10364  axcclem  10370  brdom3  10441  brdom7disj  10444  brdom6disj  10445  axpowndlem3  10513  canthnumlem  10562  canthp1lem2  10567  inar1  10689  recmulnq  10878  ltexnq  10889  halfnq  10890  ltbtwnnq  10892  1idpr  10943  ltexprlem7  10956  reclem2pr  10962  reclem3pr  10963  sup2  12103  nnunb  12424  uzrdgfni  13911  axdc4uzlem  13936  rtrclreclem3  15013  ntrivcvgmullem  15857  fprodntriv  15898  cnso  16205  vdwapun  16936  vdwlem1  16943  vdwlem12  16954  vdwlem13  16955  isacs2  17610  equivestrcsetc  18109  psgneu  19472  efglem  19682  lmisfree  21817  toprntopon  22908  neitr  23163  cmpsublem  23382  cmpsub  23383  bwth  23393  1stcfb  23428  unisngl  23510  alexsubALTlem3  24032  alexsubALTlem4  24033  vitali  25598  mbfi1fseqlem6  25705  mbfi1flimlem  25707  aannenlem2  26313  nosupno  27685  nosupfv  27688  noinfno  27700  noinffv  27703  noseqrdgfn  28316  istrkg2ld  28546  axlowdim  29048  wlkswwlksf1o  29965  clwlkclwwlkf  30096  padct  32810  f1ocnt  32892  cycpmconjslem2  33236  locfinreflem  34024  locfinref  34025  prsdm  34098  prsrn  34099  eulerpart  34566  fineqvac  35297  satf0op  35605  prv1n  35659  fnsingle  36145  finminlem  36546  filnetlem3  36608  dfttc4lem1  36756  regsfromregtco  36766  cnndvlem2  36844  bj-restpw  37450  bj-rest0  37451  exrecfnlem  37741  ctbssinf  37768  poimirlem2  37989  mblfinlem3  38026  mblfinlem4  38027  ismblfin  38028  itg2addnclem  38038  itg2addnc  38041  indexdom  38101  sdclem2  38109  fdc  38112  prtlem16  39361  dihglblem2aN  41785  sn-sup2  42981  eldioph2lem2  43210  dford3lem2  43472  aomclem7  43505  dfac11  43507  rclexi  44059  trclexi  44064  rtrclexi  44065  permaxinf2lem  45456  permac8prim  45458  fnchoice  45477  ssnnf1octb  45641  fzisoeu  45748  stoweidlem28  46471  nnfoctbdjlem  46898  smfpimcclem  47250  funressndmafv2rn  47686  mof0  49328  nelsubc3lem  49560  initc  49581  setc2othin  49956  cnelsubclem  50093  setrec1lem3  50179  setrec2lem2  50184