Theorem in0 4418

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

Syntax hints:   ∧ wa 395   = wceq 1537   ∈ wcel 2108   ∩ cin 3975  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-in 3983  df-nul 4353

This theorem is referenced by:  0in  4420  csbin  4465  res0  6013  dfpo2  6327  predprc  6370  fresaun  6792  oev2  8579  dju0en  10245  ackbij1lem13  10300  ackbij1lem16  10303  incexclem  15884  bitsinv1  16488  bitsinvp1  16495  sadcadd  16504  sadadd2  16506  sadid1  16514  bitsres  16519  smumullem  16538  ressbas  17293  ressbasOLD  17294  sylow2a  19661  ablfac1eu  20117  indistopon  23029  fctop  23032  cctop  23034  rest0  23198  filconn  23912  volinun  25600  itg2cnlem2  25817  pthdlem2  29804  0pth  30157  1pthdlem2  30168  disjdifprg  32597  disjun0  32617  ofpreima2  32684  of0r  32696  ldgenpisyslem1  34127  0elcarsg  34272  carsgclctunlem1  34282  carsgclctunlem3  34285  ballotlemfval0  34460  sate0  35383  elima4  35739  bj-rest10  37054  bj-rest0  37059  mblfinlem2  37618  conrel1d  43625  conrel2d  43626  ntrk0kbimka  44001  clsneibex  44064  neicvgbex  44074  qinioo  45453  nnfoctbdjlem  46376  caragen0  46427