Theorem in0 4354

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 4297	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	bianfi 533	. . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅))
3	2	bicomi 224	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅)
4	3	ineqri 4171	1 ⊢ (𝐴 ∩ ∅) = ∅

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ∩ cin 3910  ∅c0 4292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-dif 3914  df-in 3918  df-nul 4293

This theorem is referenced by:  0in  4356  csbin  4401  res0  5943  dfpo2  6257  predprc  6299  fresaun  6713  oev2  8464  dju0en  10105  ackbij1lem13  10160  ackbij1lem16  10163  incexclem  15778  bitsinv1  16388  bitsinvp1  16395  sadcadd  16404  sadadd2  16406  sadid1  16414  bitsres  16419  smumullem  16438  ressbas  17182  sylow2a  19525  ablfac1eu  19981  indistopon  22864  fctop  22867  cctop  22869  rest0  23032  filconn  23746  volinun  25423  itg2cnlem2  25639  pthdlem2  29671  0pth  30027  1pthdlem2  30038  disjdifprg  32477  disjun0  32497  ofpreima2  32563  of0r  32575  ldgenpisyslem1  34126  0elcarsg  34271  carsgclctunlem1  34281  carsgclctunlem3  34284  ballotlemfval0  34460  sate0  35375  elima4  35736  bj-rest10  37049  bj-rest0  37054  mblfinlem2  37625  conrel1d  43625  conrel2d  43626  ntrk0kbimka  44001  clsneibex  44064  neicvgbex  44074  qinioo  45506  nnfoctbdjlem  46426  caragen0  46477  resinsnALT  48834