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 4264 | . . . 4 ⊢ ¬ 𝑥 ∈ ∅ | |
2 | 1 | bianfi 534 | . . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅)) |
3 | 2 | bicomi 223 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅) |
4 | 3 | ineqri 4138 | 1 ⊢ (𝐴 ∩ ∅) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 396 = wceq 1539 ∈ wcel 2106 ∩ cin 3886 ∅c0 4256 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3434 df-dif 3890 df-in 3894 df-nul 4257 |
This theorem is referenced by: 0in 4327 csbin 4373 res0 5895 dfpo2 6199 predprc 6241 fresaun 6645 oev2 8353 dju0en 9931 ackbij1lem13 9988 ackbij1lem16 9991 incexclem 15548 bitsinv1 16149 bitsinvp1 16156 sadcadd 16165 sadadd2 16167 sadid1 16175 bitsres 16180 smumullem 16199 ressbas 16947 ressbasOLD 16948 sylow2a 19224 ablfac1eu 19676 indistopon 22151 fctop 22154 cctop 22156 rest0 22320 filconn 23034 volinun 24710 itg2cnlem2 24927 pthdlem2 28136 0pth 28489 1pthdlem2 28500 disjdifprg 30914 disjun0 30934 ofpreima2 31003 ldgenpisyslem1 32131 0elcarsg 32274 carsgclctunlem1 32284 carsgclctunlem3 32287 ballotlemfval0 32462 sate0 33377 elima4 33750 bj-rest10 35259 bj-rest0 35264 mblfinlem2 35815 conrel1d 41271 conrel2d 41272 ntrk0kbimka 41649 clsneibex 41712 neicvgbex 41722 qinioo 43073 nnfoctbdjlem 43993 caragen0 44044 |
Copyright terms: Public domain | W3C validator |