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 4293 | . . . 4 ⊢ ¬ 𝑥 ∈ ∅ | |
2 | 1 | bianfi 534 | . . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅)) |
3 | 2 | bicomi 225 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅) |
4 | 3 | ineqri 4177 | 1 ⊢ (𝐴 ∩ ∅) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 396 = wceq 1528 ∈ wcel 2105 ∩ cin 3932 ∅c0 4288 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-v 3494 df-dif 3936 df-in 3940 df-nul 4289 |
This theorem is referenced by: 0in 4344 csbin 4388 res0 5850 fresaun 6542 oev2 8137 dju0en 9589 ackbij1lem13 9642 ackbij1lem16 9645 incexclem 15179 bitsinv1 15779 bitsinvp1 15786 sadcadd 15795 sadadd2 15797 sadid1 15805 bitsres 15810 smumullem 15829 ressbas 16542 sylow2a 18673 ablfac1eu 19124 indistopon 21537 fctop 21540 cctop 21542 rest0 21705 filconn 22419 volinun 24074 itg2cnlem2 24290 pthdlem2 27476 0pth 27831 1pthdlem2 27842 disjdifprg 30253 disjun0 30273 ofpreima2 30339 ldgenpisyslem1 31321 0elcarsg 31464 carsgclctunlem1 31474 carsgclctunlem3 31477 ballotlemfval0 31652 sate0 32559 dfpo2 32888 elima4 32916 bj-rest10 34273 bj-rest0 34278 mblfinlem2 34811 conrel1d 39886 conrel2d 39887 ntrk0kbimka 40267 clsneibex 40330 neicvgbex 40340 qinioo 41687 nnfoctbdjlem 42614 caragen0 42665 |
Copyright terms: Public domain | W3C validator |