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  3814  axpweq  4171  euotd  4254  brcogw  4796  opeldmg  4832  breldmg  4833  dmsnopg  5100  dff3im  5661  elunirn  5766  unielxp  6174  op1steq  6179  tfr0dm  6322  tfrlemibxssdm  6327  tfrlemiex  6331  tfr1onlembxssdm  6343  tfr1onlemex  6347  tfrcllembxssdm  6356  tfrcllemex  6360  frecabcl  6399  ertr  6549  f1oen3g  6753  f1dom2g  6755  f1domg  6757  dom3d  6773  en1  6798  phpelm  6865  isinfinf  6896  ordiso  7034  djudom  7091  difinfsn  7098  ctm  7107  enumct  7113  djudoml  7217  djudomr  7218  cc2lem  7264  recexnq  7388  ltexprlemrl  7608  ltexprlemru  7610  recexprlemm  7622  recexprlemloc  7629  recexprlem1ssl  7631  recexprlem1ssu  7632  axpre-suploclemres  7899  frecuzrdgtcl  10411  frecuzrdgfunlem  10418  fihasheqf1oi  10766  zfz1isolem1  10819  climeu  11303  fsum3  11394  uzwodc  12037  eltg3  13527  uptx  13744  xblm  13887  bj-2inf  14660  subctctexmid  14720