Theorem in0 4375

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ∩ cin 3930  ∅c0 4313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-dif 3934  df-in 3938  df-nul 4314

This theorem is referenced by:  0in  4377  csbin  4422  res0  5975  dfpo2  6290  predprc  6332  fresaun  6754  oev2  8540  dju0en  10195  ackbij1lem13  10250  ackbij1lem16  10253  incexclem  15857  bitsinv1  16466  bitsinvp1  16473  sadcadd  16482  sadadd2  16484  sadid1  16492  bitsres  16497  smumullem  16516  ressbas  17262  sylow2a  19605  ablfac1eu  20061  indistopon  22944  fctop  22947  cctop  22949  rest0  23112  filconn  23826  volinun  25504  itg2cnlem2  25720  pthdlem2  29755  0pth  30111  1pthdlem2  30122  disjdifprg  32561  disjun0  32581  ofpreima2  32649  of0r  32661  ldgenpisyslem1  34199  0elcarsg  34344  carsgclctunlem1  34354  carsgclctunlem3  34357  ballotlemfval0  34533  sate0  35442  elima4  35798  bj-rest10  37111  bj-rest0  37116  mblfinlem2  37687  conrel1d  43654  conrel2d  43655  ntrk0kbimka  44030  clsneibex  44093  neicvgbex  44103  qinioo  45531  nnfoctbdjlem  46451  caragen0  46502  resinsnALT  48815