|   | 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 4337 | . . . 4 ⊢ ¬ 𝑥 ∈ ∅ | |
| 2 | 1 | bianfi 533 | . . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅)) | 
| 3 | 2 | bicomi 224 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅) | 
| 4 | 3 | ineqri 4211 | 1 ⊢ (𝐴 ∩ ∅) = ∅ | 
| Colors of variables: wff setvar class | 
| Syntax hints: ∧ wa 395 = wceq 1539 ∈ wcel 2107 ∩ cin 3949 ∅c0 4332 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-fal 1552 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-v 3481 df-dif 3953 df-in 3957 df-nul 4333 | 
| This theorem is referenced by: 0in 4396 csbin 4441 res0 6000 dfpo2 6315 predprc 6358 fresaun 6778 oev2 8562 dju0en 10217 ackbij1lem13 10272 ackbij1lem16 10275 incexclem 15873 bitsinv1 16480 bitsinvp1 16487 sadcadd 16496 sadadd2 16498 sadid1 16506 bitsres 16511 smumullem 16530 ressbas 17281 ressbasOLD 17282 sylow2a 19638 ablfac1eu 20094 indistopon 23009 fctop 23012 cctop 23014 rest0 23178 filconn 23892 volinun 25582 itg2cnlem2 25798 pthdlem2 29789 0pth 30145 1pthdlem2 30156 disjdifprg 32589 disjun0 32609 ofpreima2 32677 of0r 32689 ldgenpisyslem1 34165 0elcarsg 34310 carsgclctunlem1 34320 carsgclctunlem3 34323 ballotlemfval0 34499 sate0 35421 elima4 35777 bj-rest10 37090 bj-rest0 37095 mblfinlem2 37666 conrel1d 43681 conrel2d 43682 ntrk0kbimka 44057 clsneibex 44120 neicvgbex 44130 qinioo 45553 nnfoctbdjlem 46475 caragen0 46526 resinsnALT 48779 | 
| Copyright terms: Public domain | W3C validator |