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 ⊢ (𝐴 ∈ 𝑉 → (𝜓 → ∃𝑥𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402  ∃wex 1545   ∈ wcel 2209

This proof depends on 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 proof 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 used by:  spcedv  2914  spcev  2920  elabd  2971  eqeu  2996  absneu  3783  elunii  3940  axpweq  4310  euotd  4397  brcogw  4951  opeldmg  4988  breldmg  4989  dmsnopg  5262  dff3im  5856  elunirn  5975  unielxp  6412  op1steq  6417  tfr0dm  6598  tfrlemibxssdm  6603  tfrlemiex  6607  tfr1onlembxssdm  6619  tfr1onlemex  6623  tfrcllembxssdm  6632  tfrcllemex  6636  frecabcl  6675  ertr  6827  f1oen4g  7044  f1dom4g  7045  f1oen3g  7046  f1dom2g  7048  f1domg  7050  dom3d  7066  en1  7092  en2  7118  phpelm  7174  isinfinf  7207  isfsuppfid  7297  ordiso  7382  djudom  7439  difinfsn  7446  ctm  7455  enumct  7461  djudoml  7581  djudomr  7582  cc2lem  7638  recexnq  7763  ltexprlemrl  7983  ltexprlemru  7985  recexprlemm  7997  recexprlemloc  8004  recexprlem1ssl  8006  recexprlem1ssu  8007  axpre-suploclemres  8274  frecuzrdgtcl  10869  frecuzrdgfunlem  10876  fihasheqf1oi  11247  zfz1isolem1  11313  climeu  12086  fsum3  12178  uzwodc  12838  gzsumfzval  13769  psrbagmax  15183  mplsubgfilemm  15231  eltg3  15300  uptx  15517  xblm  15660  2lgslem1  16432  upgrex  16566  vtxdumgrfival  16761  1loopgrvd2fi  16768  bj-2inf  17186  subctctexmid  17252