![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 19.8a | Structured version Visualization version Unicode version |
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 1822 for a version with a dv condition requiring fewer axioms. (Contributed by NM, 9-Jan-1993.) Allow a shortening of sp 1948. (Revised by Wolf Lammen, 13-Jan-2018.) (Proof shortened by Wolf Lammen, 8-Dec-2019.) |
Ref | Expression |
---|---|
19.8a |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax12v 1945 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ax6ev 1818 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | exim 1717 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | syl6mpi 64 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | equcoms 1875 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | ax6ev 1818 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | exlimiiv 1788 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-12 1944 |
This theorem depends on definitions: df-bi 190 df-an 377 df-ex 1675 |
This theorem is referenced by: sp 1948 19.2g 1957 19.23bi 1960 nexr 1961 19.9t 1980 19.9tOLD 1983 qexmid 2068 sbequ1 2093 ax6e 2105 exdistrf 2178 equvini 2190 2ax6e 2290 euor2 2354 2moex 2383 2euex 2384 2moswap 2387 2mo 2391 rspe 2857 rsp2eOLD 2859 ceqex 3181 mo2icl 3229 intab 4279 eusv2nf 4618 copsexg 4704 dmcosseq 5118 dminss 5272 imainss 5273 relssdmrn 5379 oprabid 6347 hta 8399 domtriomlem 8903 axextnd 9047 axrepnd 9050 axunndlem1 9051 axunnd 9052 axpowndlem2 9054 axpownd 9057 axregndlem1 9058 axregnd 9060 axacndlem1 9063 axacndlem2 9064 axacndlem3 9065 axacndlem4 9066 axacndlem5 9067 axacnd 9068 fpwwe 9102 pwfseqlem4a 9117 pwfseqlem4 9118 reclem2pr 9504 bnj1121 29844 bnj1189 29868 finminlem 31024 amosym1 31136 bj-ssbft 31301 bj-19.23bit 31330 bj-nexrt 31331 bj-19.9htbi 31343 bj-nfdiOLD 31490 bj-finsumval0 31748 isbasisrelowllem1 31804 isbasisrelowllem2 31805 wl-exeq 31913 ax12indn 32560 pm11.58 36785 axc11next 36802 iotavalsb 36829 vk15.4j 36930 onfrALTlem1 36959 onfrALTlem1VD 37328 vk15.4jVD 37352 suprnmpt 37493 ssfiunibd 37602 ovncvrrp 38493 19.8ad 40806 |
Copyright terms: Public domain | W3C validator |