Theorem in0 4392

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

Syntax hints:   ∧ wa 395   = wceq 1534   ∈ wcel 2099   ∩ cin 3946  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-dif 3950  df-in 3954  df-nul 4324

This theorem is referenced by:  0in  4394  csbin  4440  res0  5989  dfpo2  6300  predprc  6344  fresaun  6768  oev2  8543  dju0en  10198  ackbij1lem13  10255  ackbij1lem16  10258  incexclem  15814  bitsinv1  16416  bitsinvp1  16423  sadcadd  16432  sadadd2  16434  sadid1  16442  bitsres  16447  smumullem  16466  ressbas  17214  ressbasOLD  17215  sylow2a  19573  ablfac1eu  20029  indistopon  22903  fctop  22906  cctop  22908  rest0  23072  filconn  23786  volinun  25474  itg2cnlem2  25691  pthdlem2  29581  0pth  29934  1pthdlem2  29945  disjdifprg  32364  disjun0  32384  ofpreima2  32451  ldgenpisyslem1  33782  0elcarsg  33927  carsgclctunlem1  33937  carsgclctunlem3  33940  ballotlemfval0  34115  sate0  35025  elima4  35371  bj-rest10  36567  bj-rest0  36572  mblfinlem2  37131  conrel1d  43093  conrel2d  43094  ntrk0kbimka  43469  clsneibex  43532  neicvgbex  43542  qinioo  44920  nnfoctbdjlem  45843  caragen0  45894