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 4217 | . . . 4 ⊢ ¬ 𝑥 ∈ ∅ | |
2 | 1 | bianfi 537 | . . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅)) |
3 | 2 | bicomi 227 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅) |
4 | 3 | ineqri 4093 | 1 ⊢ (𝐴 ∩ ∅) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 399 = wceq 1542 ∈ wcel 2113 ∩ cin 3840 ∅c0 4209 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3399 df-dif 3844 df-in 3848 df-nul 4210 |
This theorem is referenced by: 0in 4279 csbin 4326 res0 5823 fresaun 6543 oev2 8172 dju0en 9668 ackbij1lem13 9725 ackbij1lem16 9728 incexclem 15277 bitsinv1 15878 bitsinvp1 15885 sadcadd 15894 sadadd2 15896 sadid1 15904 bitsres 15909 smumullem 15928 ressbas 16650 sylow2a 18855 ablfac1eu 19307 indistopon 21745 fctop 21748 cctop 21750 rest0 21913 filconn 22627 volinun 24291 itg2cnlem2 24507 pthdlem2 27701 0pth 28054 1pthdlem2 28065 disjdifprg 30480 disjun0 30500 ofpreima2 30570 ldgenpisyslem1 31693 0elcarsg 31836 carsgclctunlem1 31846 carsgclctunlem3 31849 ballotlemfval0 32024 sate0 32940 dfpo2 33286 elima4 33314 bj-rest10 34869 bj-rest0 34874 mblfinlem2 35427 conrel1d 40801 conrel2d 40802 ntrk0kbimka 41179 clsneibex 41242 neicvgbex 41252 qinioo 42597 nnfoctbdjlem 43519 caragen0 43570 |
Copyright terms: Public domain | W3C validator |