Theorem spcev 3596

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540  ∃wex 1780   ∈ wcel 2105  Vcvv 3473

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 1912  ax-6 1970  ax-7 2010  ax-8 2107

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-clel 2809

This theorem is referenced by:  dtruALT  5386  nnullss  5462  exss  5463  euotd  5513  opeldm  5907  elrnmpt1  5957  xpnz  6158  ssimaex  6976  fvelrn  7078  dff3  7101  exfo  7106  eufnfv  7233  elunirn  7253  fsnex  7284  f1prex  7285  foeqcnvco  7301  ffoss  7936  op1steq  8023  frxp  8117  suppimacnv  8164  seqomlem2  8457  domtr  9009  en1  9027  en1OLD  9028  enfixsn  9087  ssfiALT  9180  php3  9218  php3OLD  9230  1sdomOLD  9255  isinf  9266  isinfOLD  9267  ac6sfi  9293  hartogslem1  9543  brwdom2  9574  inf0  9622  axinf2  9641  cnfcom3clem  9706  ssttrcl  9716  ttrcltr  9717  ttrclss  9721  ttrclselem2  9727  tz9.1c  9731  rankuni  9864  scott0  9887  bnd2  9894  cardprclem  9980  dfac4  10123  dfac5lem5  10128  dfac5  10129  dfac2a  10130  dfac2b  10131  kmlem2  10152  kmlem13  10163  ackbij2  10244  cfsuc  10258  cfflb  10260  cfss  10266  cfsmolem  10271  cfcoflem  10273  fin23lem32  10345  axcc2lem  10437  axcc3  10439  axdc2lem  10449  axdc3lem2  10452  axcclem  10458  brdom3  10529  brdom7disj  10532  brdom6disj  10533  axpowndlem3  10600  canthnumlem  10649  canthp1lem2  10654  inar1  10776  recmulnq  10965  ltexnq  10976  halfnq  10977  ltbtwnnq  10979  1idpr  11030  ltexprlem7  11043  reclem2pr  11049  reclem3pr  11050  sup2  12177  nnunb  12475  uzrdgfni  13930  axdc4uzlem  13955  rtrclreclem3  15014  ntrivcvgmullem  15854  fprodntriv  15893  cnso  16197  vdwapun  16914  vdwlem1  16921  vdwlem12  16932  vdwlem13  16933  isacs2  17604  equivestrcsetc  18111  psgneu  19419  efglem  19629  lmisfree  21620  toprntopon  22660  neitr  22917  cmpsublem  23136  cmpsub  23137  bwth  23147  1stcfb  23182  unisngl  23264  alexsubALTlem3  23786  alexsubALTlem4  23787  vitali  25375  mbfi1fseqlem6  25483  mbfi1flimlem  25485  aannenlem2  26092  nosupno  27457  nosupfv  27460  noinfno  27472  noinffv  27475  istrkg2ld  27993  axlowdim  28501  wlkswwlksf1o  29415  clwlkclwwlkf  29543  padct  32226  cnvoprabOLD  32227  f1ocnt  32295  cycpmconjslem2  32599  locfinreflem  33133  locfinref  33134  prsdm  33207  prsrn  33208  eulerpart  33694  fineqvac  34410  satf0op  34681  prv1n  34735  fnsingle  35210  finminlem  35519  filnetlem3  35581  cnndvlem2  35730  bj-restpw  36289  bj-rest0  36290  exrecfnlem  36576  ctbssinf  36603  poimirlem2  36806  mblfinlem3  36843  mblfinlem4  36844  ismblfin  36845  itg2addnclem  36855  itg2addnc  36858  indexdom  36918  sdclem2  36926  fdc  36929  prtlem16  38055  dihglblem2aN  40480  sn-sup2  41657  eldioph2lem2  41814  dford3lem2  42081  aomclem7  42117  dfac11  42119  rclexi  42681  trclexi  42686  rtrclexi  42687  fnchoice  44028  ssnnf1octb  44204  fzisoeu  44321  stoweidlem28  45055  nnfoctbdjlem  45482  smfpimcclem  45834  funressndmafv2rn  46242  mof0  47604  setc2othin  47776  setrec1lem3  47834  setrec2lem2  47839