MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  19.8a Unicode version

Theorem 19.8a 1857
Description: If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89. See 19.8v 1753 for a version requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 1859. (Revised by Wolf Lammen, 13-Jan-2018.) (Proof shortened by Wolf Lammen, 8-Dec-2019.)
Assertion
Ref Expression
19.8a

Proof of Theorem 19.8a
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ax6ev 1749 . 2
2 ax12v 1855 . . . . 5
3 ax6ev 1749 . . . . 5
4 exim 1654 . . . . 5
52, 3, 4syl6mpi 62 . . . 4
65equcoms 1795 . . 3
76exlimiv 1722 . 2
81, 7ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  A.wal 1393  E.wex 1612
This theorem is referenced by:  sp  1859  19.2g  1868  19.23bi  1871  nexr  1872  19.9t  1890  nfdiOLD  1963  qexmid  1977  sbequ1  1991  ax6e  2002  exdistrf  2075  equvini  2087  2ax6e  2194  ax12indn  2273  mo2vOLD  2290  mo2vOLDOLD  2291  euor2  2333  mo2OLD  2334  2moex  2365  2euex  2366  2moswap  2369  2mo  2373  2moOLD  2374  rspe  2915  rsp2eOLD  2917  ceqex  3230  mo2icl  3278  intab  4317  eusv2nf  4650  copsexg  4737  copsexgOLD  4738  dmcosseq  5269  dminss  5425  imainss  5426  relssdmrn  5533  oprabid  6323  hta  8336  domtriomlem  8843  axextnd  8987  axrepnd  8990  axunndlem1  8991  axunnd  8992  axpowndlem2  8994  axpowndlem2OLD  8995  axpownd  8999  axregndlem1  9000  axregnd  9002  axregndOLD  9003  axacndlem1  9006  axacndlem2  9007  axacndlem3  9008  axacndlem4  9009  axacndlem5  9010  axacnd  9011  fpwwe  9045  pwfseqlem4a  9060  pwfseqlem4  9061  reclem2pr  9447  amosym1  29891  wl-exeq  29987  finminlem  30136  pm11.58  31296  axc11next  31313  iotavalsb  31340  suprnmpt  31451  ssfiunibd  31509  19.8ad  33111  vk15.4j  33298  onfrALTlem1  33320  onfrALTlem1VD  33690  vk15.4jVD  33714  bnj1121  34041  bnj1189  34065  bj-19.23bit  34244  bj-nexrt  34245  bj-19.9htbi  34257  bj-finsumval0  34663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator