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

Theorem spcev 2780
 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
spcv.2
Assertion
Ref Expression
spcev
Distinct variable groups:   ,   ,
Allowed substitution hint:   ()

Proof of Theorem spcev
StepHypRef Expression
1 spcv.1 . 2
2 spcv.2 . . 3
32spcegv 2774 . 2
41, 3ax-mp 5 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 104   wceq 1331  wex 1468   wcel 1480  cvv 2686 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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121 This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688 This theorem is referenced by:  bnd2  4097  mss  4148  exss  4149  snnex  4369  opeldm  4742  elrnmpt1  4790  xpmlem  4959  ffoss  5399  ssimaex  5482  fvelrn  5551  eufnfv  5648  foeqcnvco  5691  cnvoprab  6131  domtr  6679  ensn1  6690  ac6sfi  6792  difinfsn  6985  0ct  6992  ctmlemr  6993  ctssdclemn0  6995  ctssdclemr  6997  ctssdc  6998  omct  7002  ctssexmid  7024  exmidfodomrlemim  7057  cc3  7083  zfz1iso  10591  ennnfonelemim  11943  ctinfom  11947  ctinf  11949  qnnen  11950  enctlem  11951  ctiunct  11959  subctctexmid  13249
 Copyright terms: Public domain W3C validator