Theorem spcegv 2818

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1348  ∃wex 1485   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732

This theorem is referenced by:  spcedv  2819  spcev  2825  elabd  2875  eqeu  2900  absneu  3655  elunii  3801  axpweq  4157  euotd  4239  brcogw  4780  opeldmg  4816  breldmg  4817  dmsnopg  5082  dff3im  5641  elunirn  5745  unielxp  6153  op1steq  6158  tfr0dm  6301  tfrlemibxssdm  6306  tfrlemiex  6310  tfr1onlembxssdm  6322  tfr1onlemex  6326  tfrcllembxssdm  6335  tfrcllemex  6339  frecabcl  6378  ertr  6528  f1oen3g  6732  f1dom2g  6734  f1domg  6736  dom3d  6752  en1  6777  phpelm  6844  isinfinf  6875  ordiso  7013  djudom  7070  difinfsn  7077  ctm  7086  enumct  7092  djudoml  7196  djudomr  7197  cc2lem  7228  recexnq  7352  ltexprlemrl  7572  ltexprlemru  7574  recexprlemm  7586  recexprlemloc  7593  recexprlem1ssl  7595  recexprlem1ssu  7596  axpre-suploclemres  7863  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  fihasheqf1oi  10722  zfz1isolem1  10775  climeu  11259  fsum3  11350  uzwodc  11992  eltg3  12851  uptx  13068  xblm  13211  bj-2inf  13973  subctctexmid  14034