Theorem in0 4335

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

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ∩ cin 3888  ∅c0 4273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-in 3896  df-nul 4274

This theorem is referenced by:  0in  4337  csbin  4382  res0  5948  dfpo2  6260  predprc  6302  fresaun  6711  oev2  8458  dju0en  10098  ackbij1lem13  10153  ackbij1lem16  10156  incexclem  15801  bitsinv1  16411  bitsinvp1  16418  sadcadd  16427  sadadd2  16429  sadid1  16437  bitsres  16442  smumullem  16461  ressbas  17206  sylow2a  19594  ablfac1eu  20050  indistopon  22966  fctop  22969  cctop  22971  rest0  23134  filconn  23848  volinun  25513  itg2cnlem2  25729  pthdlem2  29836  0pth  30195  1pthdlem2  30206  disjdifprg  32645  disjun0  32665  ofpreima2  32739  of0r  32752  ldgenpisyslem1  34307  0elcarsg  34451  carsgclctunlem1  34461  carsgclctunlem3  34464  ballotlemfval0  34640  sate0  35597  elima4  35958  bj-rest10  37400  bj-rest0  37405  mblfinlem2  37979  conrel1d  44090  conrel2d  44091  ntrk0kbimka  44466  clsneibex  44529  neicvgbex  44539  qinioo  45965  nnfoctbdjlem  46883  caragen0  46934  resinsnALT  49348