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 4295 | . . . 4 ⊢ ¬ 𝑥 ∈ ∅ | |
2 | 1 | bianfi 534 | . . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅)) |
3 | 2 | bicomi 225 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅) |
4 | 3 | ineqri 4179 | 1 ⊢ (𝐴 ∩ ∅) = ∅ |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 396 = wceq 1528 ∈ wcel 2105 ∩ cin 3934 ∅c0 4290 |
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 2793 |
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 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3497 df-dif 3938 df-in 3942 df-nul 4291 |
This theorem is referenced by: 0in 4346 csbin 4390 res0 5851 fresaun 6543 oev2 8139 dju0en 9590 ackbij1lem13 9643 ackbij1lem16 9646 incexclem 15181 bitsinv1 15781 bitsinvp1 15788 sadcadd 15797 sadadd2 15799 sadid1 15807 bitsres 15812 smumullem 15831 ressbas 16544 sylow2a 18675 ablfac1eu 19126 indistopon 21539 fctop 21542 cctop 21544 rest0 21707 filconn 22421 volinun 24076 itg2cnlem2 24292 pthdlem2 27477 0pth 27832 1pthdlem2 27843 disjdifprg 30254 disjun0 30274 ofpreima2 30340 ldgenpisyslem1 31322 0elcarsg 31465 carsgclctunlem1 31475 carsgclctunlem3 31478 ballotlemfval0 31653 sate0 32560 dfpo2 32889 elima4 32917 bj-rest10 34274 bj-rest0 34279 mblfinlem2 34812 conrel1d 39888 conrel2d 39889 ntrk0kbimka 40269 clsneibex 40332 neicvgbex 40342 qinioo 41691 nnfoctbdjlem 42618 caragen0 42669 |
Copyright terms: Public domain | W3C validator |