Theorem in0 3920

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 3878	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	bianfi 962	. . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅))
3	2	bicomi 213	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅)
4	3	ineqri 3768	1 ⊢ (𝐴 ∩ ∅) = ∅

Syntax hints:   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ∩ cin 3539  ∅c0 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-in 3547  df-nul 3875

This theorem is referenced by:  0in  3921  csbin  3962  res0  5321  fresaun  5988  oev2  7490  cda0en  8884  ackbij1lem13  8937  ackbij1lem16  8940  incexclem  14407  bitsinv1  15002  bitsinvp1  15009  sadcadd  15018  sadadd2  15020  sadid1  15028  bitsres  15033  smumullem  15052  ressbas  15757  sylow2a  17857  ablfac1eu  18295  indistopon  20615  fctop  20618  cctop  20620  rest0  20783  filcon  21497  volinun  23121  itg2cnlem2  23335  0pth  26100  1pthonlem2  26120  disjdifprg  28770  disjun0  28790  ofpreima2  28849  ldgenpisyslem1  29553  0elcarsg  29696  carsgclctunlem1  29706  carsgclctunlem3  29709  ballotlemfval0  29884  dfpo2  30898  elima4  30924  bj-rest10  32222  bj-rest0  32227  mblfinlem2  32617  conrel1d  36974  conrel2d  36975  ntrkbimka  37356  ntrk0kbimka  37357  clsneibex  37420  neicvgbex  37430  qinioo  38609  nnfoctbdjlem  39348  caragen0  39396  pthdlem2  40974  0pth-av  41293  1pthdlem2  41303