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 3919 | . . . 4 | |
2 | 1 | bianfi 966 | . . 3 |
3 | 2 | bicomi 214 | . 2 |
4 | 3 | ineqri 3806 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wa 384 wceq 1483 wcel 1990 cin 3573 c0 3915 |
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-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-dif 3577 df-in 3581 df-nul 3916 |
This theorem is referenced by: 0in 3969 csbin 4010 res0 5400 fresaun 6075 oev2 7603 cda0en 9001 ackbij1lem13 9054 ackbij1lem16 9057 incexclem 14568 bitsinv1 15164 bitsinvp1 15171 sadcadd 15180 sadadd2 15182 sadid1 15190 bitsres 15195 smumullem 15214 ressbas 15930 sylow2a 18034 ablfac1eu 18472 indistopon 20805 fctop 20808 cctop 20810 rest0 20973 filconn 21687 volinun 23314 itg2cnlem2 23529 pthdlem2 26664 0pth 26986 1pthdlem2 26996 disjdifprg 29388 disjun0 29408 ofpreima2 29466 ldgenpisyslem1 30226 0elcarsg 30369 carsgclctunlem1 30379 carsgclctunlem3 30382 ballotlemfval0 30557 dfpo2 31645 elima4 31679 bj-rest10 33041 bj-rest0 33046 mblfinlem2 33447 conrel1d 37955 conrel2d 37956 ntrk0kbimka 38337 clsneibex 38400 neicvgbex 38410 qinioo 39762 nnfoctbdjlem 40672 caragen0 40720 |
Copyright terms: Public domain | W3C validator |