Theorem spcev 2914

Description: Existential specialization, using implicit substitution. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)

Hypotheses

Ref	Expression
spcv.1	⊢ 𝐴 ∈ V
spcv.2	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
spcev	⊢ (𝜓 → ∃𝑥𝜑)

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem spcev

Step	Hyp	Ref	Expression
1		spcv.1	. 2 ⊢ 𝐴 ∈ V
2		spcv.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3	2	spcegv 2907	. 2 ⊢ (𝐴 ∈ V → (𝜓 → ∃𝑥𝜑))
4	1, 3	ax-mp 5	1 ⊢ (𝜓 → ∃𝑥𝜑)

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398  ∃wex 1541   ∈ wcel 2205  Vcvv 2815

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817

This theorem is referenced by:  bnd2  4291  mss  4347  exss  4348  snnex  4574  opeldm  4964  elrnmpt1  5013  xpmlem  5188  ffoss  5652  ssimaex  5743  fvelrn  5813  funopsn  5865  eufnfv  5922  foeqcnvco  5969  cnvoprab  6443  domtr  7038  ensn1  7049  ac6sfi  7168  difinfsn  7404  0ct  7411  ctmlemr  7412  ctssdclemn0  7414  ctssdclemr  7416  ctssdc  7417  omct  7421  ctssexmid  7454  exmidfodomrlemim  7517  cc3  7598  zfz1iso  11238  fzf1o  12086  fprodntrivap  12295  nninfct  12762  ennnfonelemim  13259  ctinfom  13263  ctinf  13265  qnnen  13266  enctlem  13267  ctiunct  13275  nninfdc  13288  subctctexmid  16900  domomsubct  16901