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

Syntax hints:   ∧ wa 397   = wceq 1548   ∈ wcel 2121   ∩ cin 3883  ∅c0 4263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-dif 3887  df-in 3891  df-nul 4264

This theorem is referenced by:  0in  4327  csbin  4372  res0  5941  dfpo2  6250  predprc  6292  fresaun  6701  oev2  8452  dju0en  10093  ackbij1lem13  10148  ackbij1lem16  10151  incexclem  15796  bitsinv1  16406  bitsinvp1  16413  sadcadd  16422  sadadd2  16424  sadid1  16432  bitsres  16437  smumullem  16456  ressbas  17201  sylow2a  19588  ablfac1eu  20044  indistopon  22987  fctop  22990  cctop  22992  rest0  23155  filconn  23869  volinun  25534  itg2cnlem2  25750  pthdlem2  29856  0pth  30215  1pthdlem2  30226  disjdifprg  32666  disjun0  32686  ofpreima2  32760  of0r  32773  ldgenpisyslem1  34357  0elcarsg  34501  carsgclctunlem1  34511  carsgclctunlem3  34514  ballotlemfval0  34690  sate0  35656  elima4  36017  bj-rest10  37459  bj-rest0  37464  mblfinlem2  38038  conrel1d  44120  conrel2d  44121  ntrk0kbimka  44496  clsneibex  44559  neicvgbex  44569  qinioo  45992  nnfoctbdjlem  46910  caragen0  46961  resinsnALT  49375