Theorem in0 3811

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	|- ( A i^i (/) ) = (/)

Proof of Theorem in0

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		noel 3789	. . . 4 |- -. x e. (/)
2	1	bianfi 923	. . 3 |- ( x e. (/) <-> ( x e. A /\ x e. (/) ) )
3	2	bicomi 202	. 2 |- ( ( x e. A /\ x e. (/) ) <-> x e. (/) )
4	3	ineqri 3692	1 |- ( A i^i (/) ) = (/)

Syntax hints:   /\ wa 369   = wceq 1379   e. wcel 1767   i^i cin 3475   (/)c0 3785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-dif 3479  df-in 3483  df-nul 3786

This theorem is referenced by:  csbin  3860  res0  5278  fresaun  5756  fnsuppeq0OLD  6123  fnsuppeq0  6929  oev2  7174  cda0en  8560  ackbij1lem13  8613  ackbij1lem16  8616  incexclem  13614  bitsinv1  13954  bitsinvp1  13961  sadcadd  13970  sadadd2  13972  sadid1  13980  bitsres  13985  smumullem  14004  ressbas  14548  sylow2a  16454  ablfac1eu  16938  indistopon  19308  fctop  19311  cctop  19313  rest0  19476  restsn  19477  filcon  20211  volinun  21783  itg2cnlem2  21996  chtdif  23257  ppidif  23262  ppi1  23263  cht1  23264  0pth  24345  1pthonlem2  24365  disjdifprg  27206  ofpreima2  27277  ordtconlem1  27657  measvuni  27936  measinb  27943  cndprobnul  28127  ballotlemfp1  28181  ballotlemfval0  28185  ballotlemgun  28214  mrsubvrs  28633  dfpo2  29037  elima4  29062  pred0  29132  mblfinlem2  29905  conrel1d  36998  conrel2d  36999