Theorem spcegv 2825

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353  ∃wex 1492   ∈ wcel 2148

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739

This theorem is referenced by:  spcedv  2826  spcev  2832  elabd  2882  eqeu  2907  absneu  3664  elunii  3813  axpweq  4169  euotd  4252  brcogw  4793  opeldmg  4829  breldmg  4830  dmsnopg  5097  dff3im  5658  elunirn  5762  unielxp  6170  op1steq  6175  tfr0dm  6318  tfrlemibxssdm  6323  tfrlemiex  6327  tfr1onlembxssdm  6339  tfr1onlemex  6343  tfrcllembxssdm  6352  tfrcllemex  6356  frecabcl  6395  ertr  6545  f1oen3g  6749  f1dom2g  6751  f1domg  6753  dom3d  6769  en1  6794  phpelm  6861  isinfinf  6892  ordiso  7030  djudom  7087  difinfsn  7094  ctm  7103  enumct  7109  djudoml  7213  djudomr  7214  cc2lem  7260  recexnq  7384  ltexprlemrl  7604  ltexprlemru  7606  recexprlemm  7618  recexprlemloc  7625  recexprlem1ssl  7627  recexprlem1ssu  7628  axpre-suploclemres  7895  frecuzrdgtcl  10405  frecuzrdgfunlem  10412  fihasheqf1oi  10758  zfz1isolem1  10811  climeu  11295  fsum3  11386  uzwodc  12028  eltg3  13339  uptx  13556  xblm  13699  bj-2inf  14461  subctctexmid  14521