Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > excom | Structured version Visualization version Unicode version |
Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1839, ax-6 1888, ax-7 1935, ax-10 2019, ax-12 2047. (Revised by Wolf Lammen, 8-Jan-2018.) (Proof shortened by Wolf Lammen, 22-Aug-2020.) |
Ref | Expression |
---|---|
excom |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alcom 2037 | . . 3 | |
2 | 1 | notbii 310 | . 2 |
3 | 2exnaln 1756 | . 2 | |
4 | 2exnaln 1756 | . 2 | |
5 | 2, 3, 4 | 3bitr4i 292 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wb 196 wal 1481 wex 1704 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-11 2034 |
This theorem depends on definitions: df-bi 197 df-ex 1705 |
This theorem is referenced by: excomim 2043 excom13 2044 exrot3 2045 ee4anv 2184 sbel2x 2459 2sb8e 2467 2euex 2544 2eu4 2556 rexcomf 3097 gencbvex 3250 euind 3393 sbccomlem 3508 opelopabsbALT 4984 elvvv 5178 dmuni 5334 dm0rn0 5342 dmcosseq 5387 elres 5435 rnco 5641 coass 5654 oprabid 6677 dfoprab2 6701 uniuni 6971 opabex3d 7145 opabex3 7146 frxp 7287 domen 7968 xpassen 8054 scott0 8749 dfac5lem1 8946 dfac5lem4 8949 cflem 9068 ltexprlem1 9858 ltexprlem4 9861 fsumcom2 14505 fsumcom2OLD 14506 fprodcom2 14714 fprodcom2OLD 14715 gsumval3eu 18305 dprd2d2 18443 cnvoprab 29498 eldm3 31651 dfdm5 31676 dfrn5 31677 elfuns 32022 dfiota3 32030 brimg 32044 funpartlem 32049 bj-rexcom4 32869 bj-restuni 33050 sbccom2lem 33929 diblsmopel 36460 dicelval3 36469 dihjatcclem4 36710 pm11.6 38592 ax6e2ndeq 38775 e2ebind 38779 ax6e2ndeqVD 39145 e2ebindVD 39148 e2ebindALT 39165 ax6e2ndeqALT 39167 elsprel 41725 eliunxp2 42112 |
Copyright terms: Public domain | W3C validator |