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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-in 3921  df-nul 4297

This theorem is referenced by:  0in  4360  csbin  4405  res0  5954  dfpo2  6269  predprc  6311  fresaun  6731  oev2  8487  dju0en  10129  ackbij1lem13  10184  ackbij1lem16  10187  incexclem  15802  bitsinv1  16412  bitsinvp1  16419  sadcadd  16428  sadadd2  16430  sadid1  16438  bitsres  16443  smumullem  16462  ressbas  17206  sylow2a  19549  ablfac1eu  20005  indistopon  22888  fctop  22891  cctop  22893  rest0  23056  filconn  23770  volinun  25447  itg2cnlem2  25663  pthdlem2  29698  0pth  30054  1pthdlem2  30065  disjdifprg  32504  disjun0  32524  ofpreima2  32590  of0r  32602  ldgenpisyslem1  34153  0elcarsg  34298  carsgclctunlem1  34308  carsgclctunlem3  34311  ballotlemfval0  34487  sate0  35402  elima4  35763  bj-rest10  37076  bj-rest0  37081  mblfinlem2  37652  conrel1d  43652  conrel2d  43653  ntrk0kbimka  44028  clsneibex  44091  neicvgbex  44101  qinioo  45533  nnfoctbdjlem  46453  caragen0  46504  resinsnALT  48861