Theorem in0 4356

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 4295	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	bianfi 534	. . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅))
3	2	bicomi 223	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅)
4	3	ineqri 4169	1 ⊢ (𝐴 ∩ ∅) = ∅

Syntax hints:   ∧ wa 396   = wceq 1541   ∈ wcel 2106   ∩ cin 3912  ∅c0 4287

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-dif 3916  df-in 3920  df-nul 4288

This theorem is referenced by:  0in  4358  csbin  4404  res0  5946  dfpo2  6253  predprc  6297  fresaun  6718  oev2  8474  dju0en  10120  ackbij1lem13  10177  ackbij1lem16  10180  incexclem  15732  bitsinv1  16333  bitsinvp1  16340  sadcadd  16349  sadadd2  16351  sadid1  16359  bitsres  16364  smumullem  16383  ressbas  17129  ressbasOLD  17130  sylow2a  19415  ablfac1eu  19866  indistopon  22388  fctop  22391  cctop  22393  rest0  22557  filconn  23271  volinun  24947  itg2cnlem2  25164  pthdlem2  28779  0pth  29132  1pthdlem2  29143  disjdifprg  31560  disjun0  31580  ofpreima2  31649  ldgenpisyslem1  32851  0elcarsg  32996  carsgclctunlem1  33006  carsgclctunlem3  33009  ballotlemfval0  33184  sate0  34096  elima4  34436  bj-rest10  35632  bj-rest0  35637  mblfinlem2  36189  conrel1d  42057  conrel2d  42058  ntrk0kbimka  42433  clsneibex  42496  neicvgbex  42506  qinioo  43893  nnfoctbdjlem  44816  caragen0  44867