Theorem in0 4299

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 4247	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	bianfi 537	. . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅))
3	2	bicomi 227	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅)
4	3	ineqri 4130	1 ⊢ (𝐴 ∩ ∅) = ∅

Syntax hints:   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ∩ cin 3880  ∅c0 4243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-in 3888  df-nul 4244

This theorem is referenced by:  0in  4301  csbin  4347  res0  5822  fresaun  6523  oev2  8131  dju0en  9586  ackbij1lem13  9643  ackbij1lem16  9646  incexclem  15183  bitsinv1  15781  bitsinvp1  15788  sadcadd  15797  sadadd2  15799  sadid1  15807  bitsres  15812  smumullem  15831  ressbas  16546  sylow2a  18736  ablfac1eu  19188  indistopon  21606  fctop  21609  cctop  21611  rest0  21774  filconn  22488  volinun  24150  itg2cnlem2  24366  pthdlem2  27557  0pth  27910  1pthdlem2  27921  disjdifprg  30338  disjun0  30358  ofpreima2  30429  ldgenpisyslem1  31532  0elcarsg  31675  carsgclctunlem1  31685  carsgclctunlem3  31688  ballotlemfval0  31863  sate0  32775  dfpo2  33104  elima4  33132  bj-rest10  34503  bj-rest0  34508  mblfinlem2  35095  conrel1d  40364  conrel2d  40365  ntrk0kbimka  40742  clsneibex  40805  neicvgbex  40815  qinioo  42172  nnfoctbdjlem  43094  caragen0  43145