Theorem spcegv 2913

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1402  ∃wex 1545   ∈ wcel 2209

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823

This theorem is referenced by:  spcedv  2914  spcev  2920  elabd  2971  eqeu  2996  absneu  3779  elunii  3935  axpweq  4303  euotd  4390  brcogw  4944  opeldmg  4981  breldmg  4982  dmsnopg  5254  dff3im  5844  elunirn  5962  unielxp  6398  op1steq  6403  tfr0dm  6583  tfrlemibxssdm  6588  tfrlemiex  6592  tfr1onlembxssdm  6604  tfr1onlemex  6608  tfrcllembxssdm  6617  tfrcllemex  6621  frecabcl  6660  ertr  6812  f1oen4g  7028  f1dom4g  7029  f1oen3g  7030  f1dom2g  7032  f1domg  7034  dom3d  7050  en1  7076  en2  7102  phpelm  7158  isinfinf  7191  ordiso  7366  djudom  7423  difinfsn  7430  ctm  7439  enumct  7445  djudoml  7565  djudomr  7566  cc2lem  7622  recexnq  7747  ltexprlemrl  7967  ltexprlemru  7969  recexprlemm  7981  recexprlemloc  7988  recexprlem1ssl  7990  recexprlem1ssu  7991  axpre-suploclemres  8258  frecuzrdgtcl  10827  frecuzrdgfunlem  10834  fihasheqf1oi  11204  zfz1isolem1  11270  climeu  12040  fsum3  12132  uzwodc  12792  gzsumfzval  13688  mplsubgfilemm  15012  eltg3  15081  uptx  15298  xblm  15441  2lgslem1  16124  upgrex  16258  vtxdumgrfival  16453  1loopgrvd2fi  16460  bj-2inf  16878  subctctexmid  16944