Theorem spcev 3590

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533  ∃wex 1773   ∈ wcel 2098  Vcvv 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-clel 2802

This theorem is referenced by:  dtruALT  5388  nnullss  5464  exss  5465  euotd  5515  opeldm  5910  elrnmpt1  5960  xpnz  6165  ssimaex  6982  fvelrn  7085  dff3  7109  exfo  7114  eufnfv  7241  elunirn  7261  fsnex  7292  f1prex  7293  foeqcnvco  7309  ffoss  7950  op1steq  8038  frxp  8131  suppimacnv  8179  seqomlem2  8472  domtr  9028  en1  9046  en1OLD  9047  enfixsn  9106  ssfiALT  9199  php3  9237  php3OLD  9249  1sdomOLD  9274  isinf  9285  isinfOLD  9286  ac6sfi  9312  hartogslem1  9567  brwdom2  9598  inf0  9646  axinf2  9665  cnfcom3clem  9730  ssttrcl  9740  ttrcltr  9741  ttrclss  9745  ttrclselem2  9751  tz9.1c  9755  rankuni  9888  scott0  9911  bnd2  9918  cardprclem  10004  dfac4  10147  dfac5lem5  10152  dfac5  10153  dfac2a  10154  dfac2b  10155  kmlem2  10176  kmlem13  10187  ackbij2  10268  cfsuc  10282  cfflb  10284  cfss  10290  cfsmolem  10295  cfcoflem  10297  fin23lem32  10369  axcc2lem  10461  axcc3  10463  axdc2lem  10473  axdc3lem2  10476  axcclem  10482  brdom3  10553  brdom7disj  10556  brdom6disj  10557  axpowndlem3  10624  canthnumlem  10673  canthp1lem2  10678  inar1  10800  recmulnq  10989  ltexnq  11000  halfnq  11001  ltbtwnnq  11003  1idpr  11054  ltexprlem7  11067  reclem2pr  11073  reclem3pr  11074  sup2  12203  nnunb  12501  uzrdgfni  13959  axdc4uzlem  13984  rtrclreclem3  15043  ntrivcvgmullem  15883  fprodntriv  15922  cnso  16227  vdwapun  16946  vdwlem1  16953  vdwlem12  16964  vdwlem13  16965  isacs2  17636  equivestrcsetc  18146  psgneu  19473  efglem  19683  lmisfree  21793  toprntopon  22871  neitr  23128  cmpsublem  23347  cmpsub  23348  bwth  23358  1stcfb  23393  unisngl  23475  alexsubALTlem3  23997  alexsubALTlem4  23998  vitali  25586  mbfi1fseqlem6  25694  mbfi1flimlem  25696  aannenlem2  26309  nosupno  27682  nosupfv  27685  noinfno  27697  noinffv  27700  noseqrdgfn  28229  istrkg2ld  28336  axlowdim  28844  wlkswwlksf1o  29762  clwlkclwwlkf  29890  padct  32583  cnvoprabOLD  32584  f1ocnt  32652  cycpmconjslem2  32968  locfinreflem  33572  locfinref  33573  prsdm  33646  prsrn  33647  eulerpart  34133  fineqvac  34848  satf0op  35118  prv1n  35172  fnsingle  35646  finminlem  35933  filnetlem3  35995  cnndvlem2  36144  bj-restpw  36702  bj-rest0  36703  exrecfnlem  36989  ctbssinf  37016  poimirlem2  37226  mblfinlem3  37263  mblfinlem4  37264  ismblfin  37265  itg2addnclem  37275  itg2addnc  37278  indexdom  37338  sdclem2  37346  fdc  37349  prtlem16  38471  dihglblem2aN  40896  sn-sup2  42159  eldioph2lem2  42323  dford3lem2  42590  aomclem7  42626  dfac11  42628  rclexi  43187  trclexi  43192  rtrclexi  43193  fnchoice  44533  ssnnf1octb  44706  fzisoeu  44820  stoweidlem28  45554  nnfoctbdjlem  45981  smfpimcclem  46333  funressndmafv2rn  46741  mof0  48076  setc2othin  48248  setrec1lem3  48306  setrec2lem2  48311