![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > in0 | Structured version Visualization version GIF 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 4062 | . . . 4 ⊢ ¬ 𝑥 ∈ ∅ | |
2 | 1 | bianfi 1004 | . . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅)) |
3 | 2 | bicomi 214 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅) |
4 | 3 | ineqri 3949 | 1 ⊢ (𝐴 ∩ ∅) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 383 = wceq 1632 ∈ wcel 2139 ∩ cin 3714 ∅c0 4058 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-v 3342 df-dif 3718 df-in 3722 df-nul 4059 |
This theorem is referenced by: 0in 4112 csbin 4153 res0 5555 fresaun 6236 oev2 7772 cda0en 9193 ackbij1lem13 9246 ackbij1lem16 9249 incexclem 14767 bitsinv1 15366 bitsinvp1 15373 sadcadd 15382 sadadd2 15384 sadid1 15392 bitsres 15397 smumullem 15416 ressbas 16132 sylow2a 18234 ablfac1eu 18672 indistopon 21007 fctop 21010 cctop 21012 rest0 21175 filconn 21888 volinun 23514 itg2cnlem2 23728 pthdlem2 26874 0pth 27277 1pthdlem2 27288 disjdifprg 29695 disjun0 29715 ofpreima2 29775 ldgenpisyslem1 30535 0elcarsg 30678 carsgclctunlem1 30688 carsgclctunlem3 30691 ballotlemfval0 30866 dfpo2 31952 elima4 31984 bj-rest10 33347 bj-rest0 33352 mblfinlem2 33760 conrel1d 38457 conrel2d 38458 ntrk0kbimka 38839 clsneibex 38902 neicvgbex 38912 qinioo 40265 nnfoctbdjlem 41175 caragen0 41226 |
Copyright terms: Public domain | W3C validator |