Theorem spcegv 2861

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373  ∃wex 1515   ∈ wcel 2176

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774

This theorem is referenced by:  spcedv  2862  spcev  2868  elabd  2918  eqeu  2943  absneu  3705  elunii  3855  axpweq  4215  euotd  4299  brcogw  4847  opeldmg  4883  breldmg  4884  dmsnopg  5154  dff3im  5725  elunirn  5835  unielxp  6260  op1steq  6265  tfr0dm  6408  tfrlemibxssdm  6413  tfrlemiex  6417  tfr1onlembxssdm  6429  tfr1onlemex  6433  tfrcllembxssdm  6442  tfrcllemex  6446  frecabcl  6485  ertr  6635  f1oen4g  6843  f1dom4g  6844  f1oen3g  6845  f1dom2g  6847  f1domg  6849  dom3d  6865  en1  6891  en2  6912  phpelm  6963  isinfinf  6994  ordiso  7138  djudom  7195  difinfsn  7202  ctm  7211  enumct  7217  djudoml  7331  djudomr  7332  cc2lem  7378  recexnq  7503  ltexprlemrl  7723  ltexprlemru  7725  recexprlemm  7737  recexprlemloc  7744  recexprlem1ssl  7746  recexprlem1ssu  7747  axpre-suploclemres  8014  frecuzrdgtcl  10557  frecuzrdgfunlem  10564  fihasheqf1oi  10932  zfz1isolem1  10985  climeu  11607  fsum3  11698  uzwodc  12358  gsumfzval  13223  mplsubgfilemm  14460  eltg3  14529  uptx  14746  xblm  14889  2lgslem1  15568  bj-2inf  15874  subctctexmid  15937