Theorem in0 4345

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 4296	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	bianfi 536	. . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅))
3	2	bicomi 226	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅)
4	3	ineqri 4180	1 ⊢ (𝐴 ∩ ∅) = ∅

Syntax hints:   ∧ wa 398   = wceq 1537   ∈ wcel 2114   ∩ cin 3935  ∅c0 4291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3939  df-in 3943  df-nul 4292

This theorem is referenced by:  0in  4347  csbin  4391  res0  5857  fresaun  6549  oev2  8148  dju0en  9601  ackbij1lem13  9654  ackbij1lem16  9657  incexclem  15191  bitsinv1  15791  bitsinvp1  15798  sadcadd  15807  sadadd2  15809  sadid1  15817  bitsres  15822  smumullem  15841  ressbas  16554  sylow2a  18744  ablfac1eu  19195  indistopon  21609  fctop  21612  cctop  21614  rest0  21777  filconn  22491  volinun  24147  itg2cnlem2  24363  pthdlem2  27549  0pth  27904  1pthdlem2  27915  disjdifprg  30325  disjun0  30345  ofpreima2  30411  ldgenpisyslem1  31422  0elcarsg  31565  carsgclctunlem1  31575  carsgclctunlem3  31578  ballotlemfval0  31753  sate0  32662  dfpo2  32991  elima4  33019  bj-rest10  34382  bj-rest0  34387  mblfinlem2  34945  conrel1d  40028  conrel2d  40029  ntrk0kbimka  40409  clsneibex  40472  neicvgbex  40482  qinioo  41831  nnfoctbdjlem  42757  caragen0  42808