Theorem in0 3785

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 3762	. . . 4 |- -. x e. (/)
2	1	bianfi 933	. . 3 |- ( x e. (/) <-> ( x e. A /\ x e. (/) ) )
3	2	bicomi 205	. 2 |- ( ( x e. A /\ x e. (/) ) <-> x e. (/) )
4	3	ineqri 3653	1 |- ( A i^i (/) ) = (/)

Syntax hints:   /\ wa 370   = wceq 1437   e. wcel 1867   i^i cin 3432   (/)c0 3758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080  df-dif 3436  df-in 3440  df-nul 3759

This theorem is referenced by:  csbin  3824  res0  5120  pred0  5420  fresaun  5762  fnsuppeq0  6945  oev2  7224  cda0en  8598  ackbij1lem13  8651  ackbij1lem16  8654  incexclem  13861  bitsinv1  14379  bitsinvp1  14386  sadcadd  14395  sadadd2  14397  sadid1  14405  bitsres  14410  smumullem  14429  ressbas  15139  sylow2a  17212  ablfac1eu  17647  indistopon  19953  fctop  19956  cctop  19958  rest0  20122  restsn  20123  filcon  20835  volinun  22406  itg2cnlem2  22627  chtdif  23987  ppidif  23992  ppi1  23993  cht1  23994  0pth  25186  1pthonlem2  25206  disjdifprg  28065  disjun0  28085  ofpreima2  28150  ordtconlem1  28610  ldgenpisyslem1  28865  measvuni  28916  measinb  28923  0elcarsg  29009  carsgclctunlem1  29019  carsgclctunlem3  29022  cndprobnul  29137  ballotlemfp1  29191  ballotlemfval0  29195  ballotlemgun  29224  mrsubvrs  29989  dfpo2  30223  elima4  30249  mblfinlem2  31726  conrel1d  35942  conrel2d  35943  0in  37082  nnfoctbdjlem  37850  caragen0  37884