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  4170  euotd  4253  brcogw  4795  opeldmg  4831  breldmg  4832  dmsnopg  5099  dff3im  5660  elunirn  5764  unielxp  6172  op1steq  6177  tfr0dm  6320  tfrlemibxssdm  6325  tfrlemiex  6329  tfr1onlembxssdm  6341  tfr1onlemex  6345  tfrcllembxssdm  6354  tfrcllemex  6358  frecabcl  6397  ertr  6547  f1oen3g  6751  f1dom2g  6753  f1domg  6755  dom3d  6771  en1  6796  phpelm  6863  isinfinf  6894  ordiso  7032  djudom  7089  difinfsn  7096  ctm  7105  enumct  7111  djudoml  7215  djudomr  7216  cc2lem  7262  recexnq  7386  ltexprlemrl  7606  ltexprlemru  7608  recexprlemm  7620  recexprlemloc  7627  recexprlem1ssl  7629  recexprlem1ssu  7630  axpre-suploclemres  7897  frecuzrdgtcl  10407  frecuzrdgfunlem  10414  fihasheqf1oi  10760  zfz1isolem1  10813  climeu  11297  fsum3  11388  uzwodc  12030  eltg3  13428  uptx  13645  xblm  13788  bj-2inf  14550  subctctexmid  14610