Theorem spcev 3567

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ∃wex 1812   ∈ wcel 2146  Vcvv 3457

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-clel 2840

This theorem is used by:  dtruALT  5361  nnullss  5445  exss  5446  euotd  5498  opeldm  5899  elrnmpt1  5952  xpnz  6158  ssimaex  6970  fvelrn  7075  dff3  7099  exfo  7104  eufnfv  7234  elunirn  7254  fsnex  7290  f1prex  7291  foeqcnvco  7307  ffoss  7949  op1steq  8036  frxp  8128  suppimacnv  8176  seqomlem2  8444  domtr  9010  en1  9027  enfixsn  9081  ssfiALT  9165  php3  9200  isinf  9232  ac6sfi  9251  hartogslem1  9511  brwdom2  9542  inf0  9597  axinf2  9616  cnfcom3clem  9681  ssttrcl  9691  ttrcltr  9692  ttrclss  9696  ttrclselem2  9702  tz9.1c  9706  rankuni  9842  scott0b  9873  scott0OLD  9874  bnd2  9892  cardprclem  9981  dfac4  10122  dfac5lem5  10127  dfac5  10128  dfac2a  10129  dfac2b  10130  kmlem2  10151  kmlem13  10162  ackbij2  10241  cfsuc  10256  cfflb  10258  cfss  10264  cfsmolem  10269  cfcoflem  10271  fin23lem32  10343  axcc2lem  10435  axcc3  10437  axdc2lem  10447  axdc3lem2  10450  axcclem  10456  brdom3  10527  brdom7disj  10530  brdom6disj  10531  axpowndlem3  10599  canthnumlem  10648  canthp1lem2  10653  inar1  10775  recmulnq  10964  ltexnq  10975  halfnq  10976  ltbtwnnq  10978  1idpr  11029  ltexprlem7  11042  reclem2pr  11048  reclem3pr  11049  sup2  12186  nnunb  12515  uzrdgfni  14012  axdc4uzlem  14037  rtrclreclem3  15121  ntrivcvgmullem  15978  fprodntriv  16019  cnso  16325  vdwapun  17056  vdwlem1  17063  vdwlem12  17074  vdwlem13  17075  isacs2  17731  equivestrcsetc  18230  psgneu  19620  efglem  19830  lmisfree  22042  toprntopon  23132  neitr  23387  cmpsublem  23606  cmpsub  23607  bwth  23617  1stcfb  23652  unisngl  23735  alexsubALTlem3  24257  alexsubALTlem4  24258  vitali  25823  mbfi1fseqlem6  25930  mbfi1flimlem  25932  aannenlem2  26543  nosupno  27918  nosupfv  27921  noinfno  27933  noinffv  27936  noseqrdgfn  28550  istrkg2ld  28780  axlowdim  29366  wlkswwlksf1o  30295  clwlkclwwlkf  30426  padct  33133  f1ocnt  33215  cycpmconjslem2  33539  locfinreflem  34294  locfinref  34295  prsdm  34368  prsrn  34369  eulerpart  34837  fineqvac  35586  satf0op  35906  prv1n  35960  fnsingle  36446  finminlem  36886  filnetlem3  36948  dfttc4lem1  37096  regsfromregtco  37106  cnndvlem2  37184  bj-restpw  37791  bj-rest0  37792  exrecfnlem  38082  ctbssinf  38109  poimirlem2  38330  mblfinlem3  38367  mblfinlem4  38368  ismblfin  38369  itg2addnclem  38379  itg2addnc  38382  indexdom  38443  sdclem2  38451  fdc  38454  prtlem16  39701  dihglblem2aN  42125  sn-sup2  43323  eldioph2lem2  43550  dford3lem2  43812  aomclem7  43845  dfac11  43847  rclexi  44399  trclexi  44404  rtrclexi  44405  permaxinf2lem  45779  permac8prim  45781  fnchoice  45807  ssnnf1octb  45970  fzisoeu  46077  stoweidlem28  46800  nnfoctbdjlem  47227  smfpimcclem  47579  funressndmafv2rn  48018  mof0  49673  nelsubc3lem  49905  initc  49926  setc2othin  50301  cnelsubclem  50438  setrec1lem3  50524  setrec2lem2  50529