Theorem spcegv 2848

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

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

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762

This theorem is referenced by:  spcedv  2849  spcev  2855  elabd  2905  eqeu  2930  absneu  3690  elunii  3840  axpweq  4200  euotd  4283  brcogw  4831  opeldmg  4867  breldmg  4868  dmsnopg  5137  dff3im  5703  elunirn  5809  unielxp  6227  op1steq  6232  tfr0dm  6375  tfrlemibxssdm  6380  tfrlemiex  6384  tfr1onlembxssdm  6396  tfr1onlemex  6400  tfrcllembxssdm  6409  tfrcllemex  6413  frecabcl  6452  ertr  6602  f1oen3g  6808  f1dom2g  6810  f1domg  6812  dom3d  6828  en1  6853  phpelm  6922  isinfinf  6953  ordiso  7095  djudom  7152  difinfsn  7159  ctm  7168  enumct  7174  djudoml  7279  djudomr  7280  cc2lem  7326  recexnq  7450  ltexprlemrl  7670  ltexprlemru  7672  recexprlemm  7684  recexprlemloc  7691  recexprlem1ssl  7693  recexprlem1ssu  7694  axpre-suploclemres  7961  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  fihasheqf1oi  10858  zfz1isolem1  10911  climeu  11439  fsum3  11530  uzwodc  12174  gsumfzval  12974  eltg3  14225  uptx  14442  xblm  14585  bj-2inf  15430  subctctexmid  15491