Theorem in0 4401

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

Syntax hints:   ∧ wa 395   = wceq 1537   ∈ wcel 2106   ∩ cin 3962  ∅c0 4339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-dif 3966  df-in 3970  df-nul 4340

This theorem is referenced by:  0in  4403  csbin  4448  res0  6004  dfpo2  6318  predprc  6361  fresaun  6780  oev2  8560  dju0en  10214  ackbij1lem13  10269  ackbij1lem16  10272  incexclem  15869  bitsinv1  16476  bitsinvp1  16483  sadcadd  16492  sadadd2  16494  sadid1  16502  bitsres  16507  smumullem  16526  ressbas  17280  ressbasOLD  17281  sylow2a  19652  ablfac1eu  20108  indistopon  23024  fctop  23027  cctop  23029  rest0  23193  filconn  23907  volinun  25595  itg2cnlem2  25812  pthdlem2  29801  0pth  30154  1pthdlem2  30165  disjdifprg  32595  disjun0  32615  ofpreima2  32683  of0r  32695  ldgenpisyslem1  34144  0elcarsg  34289  carsgclctunlem1  34299  carsgclctunlem3  34302  ballotlemfval0  34477  sate0  35400  elima4  35757  bj-rest10  37071  bj-rest0  37076  mblfinlem2  37645  conrel1d  43653  conrel2d  43654  ntrk0kbimka  44029  clsneibex  44092  neicvgbex  44102  qinioo  45488  nnfoctbdjlem  46411  caragen0  46462