Theorem spcegv 2891

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 2886	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 2801

This theorem is referenced by:  spcedv  2892  spcev  2898  elabd  2948  eqeu  2973  absneu  3738  elunii  3893  axpweq  4255  euotd  4341  brcogw  4891  opeldmg  4928  breldmg  4929  dmsnopg  5200  dff3im  5780  elunirn  5890  unielxp  6320  op1steq  6325  tfr0dm  6468  tfrlemibxssdm  6473  tfrlemiex  6477  tfr1onlembxssdm  6489  tfr1onlemex  6493  tfrcllembxssdm  6502  tfrcllemex  6506  frecabcl  6545  ertr  6695  f1oen4g  6903  f1dom4g  6904  f1oen3g  6905  f1dom2g  6907  f1domg  6909  dom3d  6925  en1  6951  en2  6973  phpelm  7028  isinfinf  7059  ordiso  7203  djudom  7260  difinfsn  7267  ctm  7276  enumct  7282  djudoml  7401  djudomr  7402  cc2lem  7452  recexnq  7577  ltexprlemrl  7797  ltexprlemru  7799  recexprlemm  7811  recexprlemloc  7818  recexprlem1ssl  7820  recexprlem1ssu  7821  axpre-suploclemres  8088  frecuzrdgtcl  10634  frecuzrdgfunlem  10641  fihasheqf1oi  11009  zfz1isolem1  11062  climeu  11807  fsum3  11898  uzwodc  12558  gsumfzval  13424  mplsubgfilemm  14662  eltg3  14731  uptx  14948  xblm  15091  2lgslem1  15770  upgrex  15903  bj-2inf  16301  subctctexmid  16366