Theorem in0 4111

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.)

Assertion

Ref	Expression
in0	⊢ (𝐴 ∩ ∅) = ∅

Proof of Theorem in0

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		noel 4062	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	bianfi 1004	. . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅))
3	2	bicomi 214	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅)
4	3	ineqri 3949	1 ⊢ (𝐴 ∩ ∅) = ∅

Syntax hints:   ∧ wa 383   = wceq 1632   ∈ wcel 2139   ∩ cin 3714  ∅c0 4058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-dif 3718  df-in 3722  df-nul 4059

This theorem is referenced by:  0in  4112  csbin  4153  res0  5555  fresaun  6236  oev2  7772  cda0en  9193  ackbij1lem13  9246  ackbij1lem16  9249  incexclem  14767  bitsinv1  15366  bitsinvp1  15373  sadcadd  15382  sadadd2  15384  sadid1  15392  bitsres  15397  smumullem  15416  ressbas  16132  sylow2a  18234  ablfac1eu  18672  indistopon  21007  fctop  21010  cctop  21012  rest0  21175  filconn  21888  volinun  23514  itg2cnlem2  23728  pthdlem2  26874  0pth  27277  1pthdlem2  27288  disjdifprg  29695  disjun0  29715  ofpreima2  29775  ldgenpisyslem1  30535  0elcarsg  30678  carsgclctunlem1  30688  carsgclctunlem3  30691  ballotlemfval0  30866  dfpo2  31952  elima4  31984  bj-rest10  33347  bj-rest0  33352  mblfinlem2  33760  conrel1d  38457  conrel2d  38458  ntrk0kbimka  38839  clsneibex  38902  neicvgbex  38912  qinioo  40265  nnfoctbdjlem  41175  caragen0  41226