ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  spcev GIF version

Theorem spcev 2754
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
StepHypRef Expression
1 spcv.1 . 2 𝐴 ∈ V
2 spcv.2 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32spcegv 2748 . 2 (𝐴 ∈ V → (𝜓 → ∃𝑥𝜑))
41, 3ax-mp 5 1 (𝜓 → ∃𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1316  wex 1453  wcel 1465  Vcvv 2660
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662
This theorem is referenced by:  bnd2  4067  mss  4118  exss  4119  snnex  4339  opeldm  4712  elrnmpt1  4760  xpmlem  4929  ffoss  5367  ssimaex  5450  fvelrn  5519  eufnfv  5616  foeqcnvco  5659  cnvoprab  6099  domtr  6647  ensn1  6658  ac6sfi  6760  difinfsn  6953  0ct  6960  ctmlemr  6961  ctssdclemn0  6963  ctssdclemr  6965  ctssdc  6966  omct  6970  ctssexmid  6992  exmidfodomrlemim  7025  zfz1iso  10552  ennnfonelemim  11864  ctinfom  11868  ctinf  11870  qnnen  11871  enctlem  11872  ctiunct  11880  subctctexmid  13123
  Copyright terms: Public domain W3C validator