NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  19.8a Unicode version

Theorem 19.8a 1756
Description: If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
19.8a

Proof of Theorem 19.8a
StepHypRef Expression
1 sp 1747 . . 3
21con2i 112 . 2
3 df-ex 1542 . 2
42, 3sylibr 203 1
Colors of variables: wff setvar class
Syntax hints:   wn 3   wi 4  wal 1540  wex 1541
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-ex 1542
This theorem is referenced by:  19.2g  1757  19.23bi  1759  nexr  1760  19.9t  1779  19.9hOLD  1781  19.23tOLD  1819  19.23hOLD  1820  19.9tOLD  1857  excomimOLD  1858  19.38OLD  1874  qexmid  1886  sbequ1  1918  ax12olem5  1931  ax10lem2  1937  exdistrf  1971  ax11indn  2195  mo  2226  mo2  2233  euor2  2272  2moex  2275  2euex  2276  2moswap  2279  2mo  2282  rspe  2675  rsp2e  2677  ceqex  2969  mo2icl  3015  necompl  3544  intab  3956  copsexg  4607  imainss  5042  nfunv  5138  oprabid  5550
  Copyright terms: Public domain W3C validator