Theorem spcegv 2852

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364  ∃wex 1506   ∈ wcel 2167

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765

This theorem is referenced by:  spcedv  2853  spcev  2859  elabd  2909  eqeu  2934  absneu  3695  elunii  3845  axpweq  4205  euotd  4288  brcogw  4836  opeldmg  4872  breldmg  4873  dmsnopg  5142  dff3im  5710  elunirn  5816  unielxp  6241  op1steq  6246  tfr0dm  6389  tfrlemibxssdm  6394  tfrlemiex  6398  tfr1onlembxssdm  6410  tfr1onlemex  6414  tfrcllembxssdm  6423  tfrcllemex  6427  frecabcl  6466  ertr  6616  f1oen3g  6822  f1dom2g  6824  f1domg  6826  dom3d  6842  en1  6867  phpelm  6936  isinfinf  6967  ordiso  7111  djudom  7168  difinfsn  7175  ctm  7184  enumct  7190  djudoml  7304  djudomr  7305  cc2lem  7351  recexnq  7476  ltexprlemrl  7696  ltexprlemru  7698  recexprlemm  7710  recexprlemloc  7717  recexprlem1ssl  7719  recexprlem1ssu  7720  axpre-suploclemres  7987  frecuzrdgtcl  10523  frecuzrdgfunlem  10530  fihasheqf1oi  10898  zfz1isolem1  10951  climeu  11480  fsum3  11571  uzwodc  12231  gsumfzval  13095  mplsubgfilemm  14332  eltg3  14401  uptx  14618  xblm  14761  2lgslem1  15440  bj-2inf  15692  subctctexmid  15755