Theorem spcegv 2708

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 2229	. 2 ⊢ Ⅎ𝑥𝐴
2		nfv 1467	. 2 ⊢ Ⅎ𝑥𝜓
3		spcgv.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	1, 2, 3	spcegf 2703	1 ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1290  ∃wex 1427   ∈ wcel 1439

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-v 2622

This theorem is referenced by:  spcev  2714  eqeu  2786  absneu  3518  elunii  3664  axpweq  4012  euotd  4090  brcogw  4618  opeldmg  4654  breldmg  4655  dmsnopg  4915  dff3im  5458  elunirn  5559  unielxp  5958  op1steq  5963  tfr0dm  6101  tfrlemibxssdm  6106  tfrlemiex  6110  tfr1onlembxssdm  6122  tfr1onlemex  6126  tfrcllembxssdm  6135  tfrcllemex  6139  frecabcl  6178  ertr  6321  f1oen3g  6525  f1dom2g  6527  f1domg  6529  dom3d  6545  en1  6570  phpelm  6636  isinfinf  6667  ordiso  6783  djudom  6837  ctm  6845  enumct  6847  recexnq  7010  ltexprlemrl  7230  ltexprlemru  7232  recexprlemm  7244  recexprlemloc  7251  recexprlem1ssl  7253  recexprlem1ssu  7254  frecuzrdgtcl  9880  frecuzrdgfunlem  9887  fihasheqf1oi  10257  zfz1isolem1  10306  climeu  10745  fisum  10839  eltg3  11818  bj-2inf  12106