![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > in0 | Structured version Visualization version Unicode version |
Description: The intersection of a class with the empty set is the empty set. Theorem 16 of [Suppes] p. 26. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
in0 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | noel 3747 |
. . . 4
![]() ![]() ![]() ![]() ![]() | |
2 | 1 | bianfi 941 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | bicomi 207 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | ineqri 3638 |
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-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-dif 3419 df-in 3423 df-nul 3744 |
This theorem is referenced by: csbin 3811 res0 5131 pred0 5433 fresaun 5781 fnsuppeq0 6975 oev2 7256 cda0en 8640 ackbij1lem13 8693 ackbij1lem16 8696 incexclem 13949 bitsinv1 14471 bitsinvp1 14478 sadcadd 14487 sadadd2 14489 sadid1 14497 bitsres 14502 smumullem 14521 ressbas 15234 sylow2a 17326 ablfac1eu 17761 indistopon 20071 fctop 20074 cctop 20076 rest0 20240 restsn 20241 filcon 20953 volinun 22555 itg2cnlem2 22776 chtdif 24141 ppidif 24146 ppi1 24147 cht1 24148 0pth 25356 1pthonlem2 25376 disjdifprg 28239 disjun0 28259 ofpreima2 28321 ordtconlem1 28781 ldgenpisyslem1 29036 measvuni 29087 measinb 29094 0elcarsg 29189 carsgclctunlem1 29199 carsgclctunlem3 29202 cndprobnul 29320 ballotlemfp1 29374 ballotlemfval0 29378 ballotlemgun 29407 ballotlemgunOLD 29445 mrsubvrs 30210 dfpo2 30445 elima4 30471 mblfinlem2 32024 conrel1d 36301 conrel2d 36302 0in 37432 qinioo 37722 nnfoctbdjlem 38398 caragen0 38435 pthdlem2 39890 0pth-av 39937 1pthdlem2 39947 |
Copyright terms: Public domain | W3C validator |