Theorem spcev 2867

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 2860	. 2 ⊢ (𝐴 ∈ V → (𝜓 → ∃𝑥𝜑))
4	1, 3	ax-mp 5	1 ⊢ (𝜓 → ∃𝑥𝜑)

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1372  ∃wex 1514   ∈ wcel 2175  Vcvv 2771

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773

This theorem is referenced by:  bnd2  4216  mss  4269  exss  4270  snnex  4494  opeldm  4880  elrnmpt1  4928  xpmlem  5102  ffoss  5553  ssimaex  5639  fvelrn  5710  funopsn  5761  eufnfv  5814  foeqcnvco  5858  cnvoprab  6319  domtr  6876  ensn1  6887  ac6sfi  6994  difinfsn  7201  0ct  7208  ctmlemr  7209  ctssdclemn0  7211  ctssdclemr  7213  ctssdc  7214  omct  7218  ctssexmid  7251  exmidfodomrlemim  7308  cc3  7379  zfz1iso  10984  fprodntrivap  11837  nninfct  12304  ennnfonelemim  12737  ctinfom  12741  ctinf  12743  qnnen  12744  enctlem  12745  ctiunct  12753  nninfdc  12766  subctctexmid  15870  domomsubct  15871