![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elpr | Structured version Visualization version Unicode version |
Description: A member of an unordered pair of classes is one or the other of them. Exercise 1 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.) |
Ref | Expression |
---|---|
elpr.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
elpr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpr.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | elprg 3996 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
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-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-v 3059 df-un 3421 df-sn 3981 df-pr 3983 |
This theorem is referenced by: difprsnss 4120 preqr1OLD 4162 preq12b 4164 prel12 4165 pwpr 4208 pwtp 4209 unipr 4225 intpr 4282 axpr 4655 zfpair2 4657 elopOLD 4685 opthwiener 4720 tpres 6146 fnprb 6152 2oconcl 7236 pw2f1olem 7707 sdom2en01 8763 gruun 9262 fzpr 11886 m1expeven 12357 bpoly2 14165 bpoly3 14166 lcmfpr 14655 isprm2 14687 drngnidl 18508 psgninv 19205 psgnodpm 19211 mdetunilem7 19698 indistopon 20071 dfcon2 20489 cnconn 20492 uncon 20499 txindis 20704 txcon 20759 filcon 20953 xpsdsval 21451 rolle 22998 dvivthlem1 23016 ang180lem3 23796 ang180lem4 23797 wilthlem2 24050 sqff1o 24165 ppiub 24188 lgslem1 24280 lgsdir2lem4 24310 lgsdir2lem5 24311 usgraexmplef 25184 3vfriswmgralem 25788 lmat22lem 28694 signslema 29501 subfacp1lem1 29952 subfacp1lem4 29956 nosgnn0 30595 rankeq1o 30988 onsucconi 31147 topdifinfindis 31795 poimirlem9 31995 divrngidl 32307 isfldidl 32347 dihmeetlem2N 34913 wopprc 35931 pw2f1ocnv 35938 kelac2lem 35968 rnmptpr 37498 cncfiooicclem1 37857 elmod2OLD 38861 structiedg0val 39266 gsumpr 40511 nn0sumshdiglem2 40802 |
Copyright terms: Public domain | W3C validator |