Theorem in0 4347

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

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ∩ cin 3900  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-in 3908  df-nul 4286

This theorem is referenced by:  0in  4349  csbin  4394  res0  5942  dfpo2  6254  predprc  6296  fresaun  6705  oev2  8450  dju0en  10086  ackbij1lem13  10141  ackbij1lem16  10144  incexclem  15759  bitsinv1  16369  bitsinvp1  16376  sadcadd  16385  sadadd2  16387  sadid1  16395  bitsres  16400  smumullem  16419  ressbas  17163  sylow2a  19548  ablfac1eu  20004  indistopon  22945  fctop  22948  cctop  22950  rest0  23113  filconn  23827  volinun  25503  itg2cnlem2  25719  pthdlem2  29841  0pth  30200  1pthdlem2  30211  disjdifprg  32650  disjun0  32670  ofpreima2  32744  of0r  32758  ldgenpisyslem1  34320  0elcarsg  34464  carsgclctunlem1  34474  carsgclctunlem3  34477  ballotlemfval0  34653  sate0  35609  elima4  35970  bj-rest10  37293  bj-rest0  37298  mblfinlem2  37859  conrel1d  43904  conrel2d  43905  ntrk0kbimka  44280  clsneibex  44343  neicvgbex  44353  qinioo  45781  nnfoctbdjlem  46699  caragen0  46750  resinsnALT  49118