Theorem in0 4361

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

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

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-in 3924  df-nul 4300

This theorem is referenced by:  0in  4363  csbin  4408  res0  5957  dfpo2  6272  predprc  6314  fresaun  6734  oev2  8490  dju0en  10136  ackbij1lem13  10191  ackbij1lem16  10194  incexclem  15809  bitsinv1  16419  bitsinvp1  16426  sadcadd  16435  sadadd2  16437  sadid1  16445  bitsres  16450  smumullem  16469  ressbas  17213  sylow2a  19556  ablfac1eu  20012  indistopon  22895  fctop  22898  cctop  22900  rest0  23063  filconn  23777  volinun  25454  itg2cnlem2  25670  pthdlem2  29705  0pth  30061  1pthdlem2  30072  disjdifprg  32511  disjun0  32531  ofpreima2  32597  of0r  32609  ldgenpisyslem1  34160  0elcarsg  34305  carsgclctunlem1  34315  carsgclctunlem3  34318  ballotlemfval0  34494  sate0  35409  elima4  35770  bj-rest10  37083  bj-rest0  37088  mblfinlem2  37659  conrel1d  43659  conrel2d  43660  ntrk0kbimka  44035  clsneibex  44098  neicvgbex  44108  qinioo  45540  nnfoctbdjlem  46460  caragen0  46511  resinsnALT  48865