Theorem in0 4322

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

Syntax hints:   ∧ wa 395   = wceq 1539   ∈ wcel 2108   ∩ cin 3882  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-in 3890  df-nul 4254

This theorem is referenced by:  0in  4324  csbin  4370  res0  5884  dfpo2  6188  fresaun  6629  oev2  8315  dju0en  9862  ackbij1lem13  9919  ackbij1lem16  9922  incexclem  15476  bitsinv1  16077  bitsinvp1  16084  sadcadd  16093  sadadd2  16095  sadid1  16103  bitsres  16108  smumullem  16127  ressbas  16873  ressbasOLD  16874  sylow2a  19139  ablfac1eu  19591  indistopon  22059  fctop  22062  cctop  22064  rest0  22228  filconn  22942  volinun  24615  itg2cnlem2  24832  pthdlem2  28037  0pth  28390  1pthdlem2  28401  disjdifprg  30815  disjun0  30835  ofpreima2  30905  ldgenpisyslem1  32031  0elcarsg  32174  carsgclctunlem1  32184  carsgclctunlem3  32187  ballotlemfval0  32362  sate0  33277  elima4  33656  bj-rest10  35186  bj-rest0  35191  mblfinlem2  35742  conrel1d  41160  conrel2d  41161  ntrk0kbimka  41538  clsneibex  41601  neicvgbex  41611  qinioo  42963  nnfoctbdjlem  43883  caragen0  43934