Theorem spcegv 2892

Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.)

Hypothesis

Ref	Expression
spcgv.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
spcegv	⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem spcegv

Step	Hyp	Ref	Expression
1		nfcv 2372	. 2 ⊢ Ⅎ𝑥𝐴
2		nfv 1574	. 2 ⊢ Ⅎ𝑥𝜓
3		spcgv.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	1, 2, 3	spcegf 2887	1 ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395  ∃wex 1538   ∈ wcel 2200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802

This theorem is referenced by:  spcedv  2893  spcev  2899  elabd  2949  eqeu  2974  absneu  3741  elunii  3896  axpweq  4259  euotd  4345  brcogw  4897  opeldmg  4934  breldmg  4935  dmsnopg  5206  dff3im  5788  elunirn  5902  unielxp  6332  op1steq  6337  tfr0dm  6483  tfrlemibxssdm  6488  tfrlemiex  6492  tfr1onlembxssdm  6504  tfr1onlemex  6508  tfrcllembxssdm  6517  tfrcllemex  6521  frecabcl  6560  ertr  6712  f1oen4g  6920  f1dom4g  6921  f1oen3g  6922  f1dom2g  6924  f1domg  6926  dom3d  6942  en1  6968  en2  6993  phpelm  7048  isinfinf  7079  ordiso  7226  djudom  7283  difinfsn  7290  ctm  7299  enumct  7305  djudoml  7424  djudomr  7425  cc2lem  7475  recexnq  7600  ltexprlemrl  7820  ltexprlemru  7822  recexprlemm  7834  recexprlemloc  7841  recexprlem1ssl  7843  recexprlem1ssu  7844  axpre-suploclemres  8111  frecuzrdgtcl  10664  frecuzrdgfunlem  10671  fihasheqf1oi  11039  zfz1isolem1  11094  climeu  11847  fsum3  11938  uzwodc  12598  gsumfzval  13464  mplsubgfilemm  14702  eltg3  14771  uptx  14988  xblm  15131  2lgslem1  15810  upgrex  15944  vtxdumgrfival  16104  1loopgrvd2fi  16111  bj-2inf  16469  subctctexmid  16537