Theorem in0 4394

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

Syntax hints:   ∧ wa 395   = wceq 1539   ∈ wcel 2107   ∩ cin 3949  ∅c0 4332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-dif 3953  df-in 3957  df-nul 4333

This theorem is referenced by:  0in  4396  csbin  4441  res0  6000  dfpo2  6315  predprc  6358  fresaun  6778  oev2  8562  dju0en  10217  ackbij1lem13  10272  ackbij1lem16  10275  incexclem  15873  bitsinv1  16480  bitsinvp1  16487  sadcadd  16496  sadadd2  16498  sadid1  16506  bitsres  16511  smumullem  16530  ressbas  17281  ressbasOLD  17282  sylow2a  19638  ablfac1eu  20094  indistopon  23009  fctop  23012  cctop  23014  rest0  23178  filconn  23892  volinun  25582  itg2cnlem2  25798  pthdlem2  29789  0pth  30145  1pthdlem2  30156  disjdifprg  32589  disjun0  32609  ofpreima2  32677  of0r  32689  ldgenpisyslem1  34165  0elcarsg  34310  carsgclctunlem1  34320  carsgclctunlem3  34323  ballotlemfval0  34499  sate0  35421  elima4  35777  bj-rest10  37090  bj-rest0  37095  mblfinlem2  37666  conrel1d  43681  conrel2d  43682  ntrk0kbimka  44057  clsneibex  44120  neicvgbex  44130  qinioo  45553  nnfoctbdjlem  46475  caragen0  46526  resinsnALT  48779