Theorem in0 4325

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

Syntax hints:   ∧ wa 396   = wceq 1539   ∈ wcel 2106   ∩ cin 3886  ∅c0 4256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-in 3894  df-nul 4257

This theorem is referenced by:  0in  4327  csbin  4373  res0  5895  dfpo2  6199  predprc  6241  fresaun  6645  oev2  8353  dju0en  9931  ackbij1lem13  9988  ackbij1lem16  9991  incexclem  15548  bitsinv1  16149  bitsinvp1  16156  sadcadd  16165  sadadd2  16167  sadid1  16175  bitsres  16180  smumullem  16199  ressbas  16947  ressbasOLD  16948  sylow2a  19224  ablfac1eu  19676  indistopon  22151  fctop  22154  cctop  22156  rest0  22320  filconn  23034  volinun  24710  itg2cnlem2  24927  pthdlem2  28136  0pth  28489  1pthdlem2  28500  disjdifprg  30914  disjun0  30934  ofpreima2  31003  ldgenpisyslem1  32131  0elcarsg  32274  carsgclctunlem1  32284  carsgclctunlem3  32287  ballotlemfval0  32462  sate0  33377  elima4  33750  bj-rest10  35259  bj-rest0  35264  mblfinlem2  35815  conrel1d  41271  conrel2d  41272  ntrk0kbimka  41649  clsneibex  41712  neicvgbex  41722  qinioo  43073  nnfoctbdjlem  43993  caragen0  44044