Theorem in0 4358

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 4299	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	bianfi 542	. . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅))
3	2	bicomi 227	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅)
4	3	ineqri 4173	1 ⊢ (𝐴 ∩ ∅) = ∅

Syntax hints:   ∧ wa 400   = wceq 1567   ∈ wcel 2149   ∩ cin 3912  ∅c0 4294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-in 3920  df-nul 4295

This theorem is referenced by:  0in  4360  csbin  4405  res0  5980  dfpo2  6294  predprc  6336  fresaun  6747  oev2  8504  dju0en  10155  ackbij1lem13  10210  ackbij1lem16  10213  incexclem  15886  bitsinv1  16496  bitsinvp1  16503  sadcadd  16512  sadadd2  16514  sadid1  16522  bitsres  16527  smumullem  16546  ressbas  17292  sylow2a  19685  ablfac1eu  20141  indistopon  23123  fctop  23126  cctop  23128  rest0  23291  filconn  24005  volinun  25670  itg2cnlem2  25886  pthdlem2  30054  0pth  30413  1pthdlem2  30424  disjdifprg  32857  disjun0  32877  ofpreima2  32948  of0r  32961  ldgenpisyslem1  34494  0elcarsg  34638  carsgclctunlem1  34648  carsgclctunlem3  34651  ballotlemfval0  34827  sate0  35802  elima4  36163  bj-rest10  37613  bj-rest0  37618  mblfinlem2  38192  conrel1d  44274  conrel2d  44275  ntrk0kbimka  44650  clsneibex  44713  neicvgbex  44723  qinioo  46136  nnfoctbdjlem  47054  caragen0  47105  resinsnALT  49529