Theorem in0 4277

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 4217	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	bianfi 537	. . 3 ⊢ (𝑥 ∈ ∅ ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅))
3	2	bicomi 227	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅)
4	3	ineqri 4093	1 ⊢ (𝐴 ∩ ∅) = ∅

Syntax hints:   ∧ wa 399   = wceq 1542   ∈ wcel 2113   ∩ cin 3840  ∅c0 4209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399  df-dif 3844  df-in 3848  df-nul 4210

This theorem is referenced by:  0in  4279  csbin  4326  res0  5823  fresaun  6543  oev2  8172  dju0en  9668  ackbij1lem13  9725  ackbij1lem16  9728  incexclem  15277  bitsinv1  15878  bitsinvp1  15885  sadcadd  15894  sadadd2  15896  sadid1  15904  bitsres  15909  smumullem  15928  ressbas  16650  sylow2a  18855  ablfac1eu  19307  indistopon  21745  fctop  21748  cctop  21750  rest0  21913  filconn  22627  volinun  24291  itg2cnlem2  24507  pthdlem2  27701  0pth  28054  1pthdlem2  28065  disjdifprg  30480  disjun0  30500  ofpreima2  30570  ldgenpisyslem1  31693  0elcarsg  31836  carsgclctunlem1  31846  carsgclctunlem3  31849  ballotlemfval0  32024  sate0  32940  dfpo2  33286  elima4  33314  bj-rest10  34869  bj-rest0  34874  mblfinlem2  35427  conrel1d  40801  conrel2d  40802  ntrk0kbimka  41179  clsneibex  41242  neicvgbex  41252  qinioo  42597  nnfoctbdjlem  43519  caragen0  43570