Theorem in0 3684

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 3662	. . . 4 |- -. x e. (/)
2	1	bianfi 916	. . 3 |- ( x e. (/) <-> ( x e. A /\ x e. (/) ) )
3	2	bicomi 202	. 2 |- ( ( x e. A /\ x e. (/) ) <-> x e. (/) )
4	3	ineqri 3565	1 |- ( A i^i (/) ) = (/)

Syntax hints:   /\ wa 369   = wceq 1369   e. wcel 1756   i^i cin 3348   (/)c0 3658

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2995  df-dif 3352  df-in 3356  df-nul 3659

This theorem is referenced by:  csbin  3733  res0  5136  fresaun  5603  fnsuppeq0OLD  5960  fnsuppeq0  6738  oev2  6984  cda0en  8369  ackbij1lem13  8422  ackbij1lem16  8425  incexclem  13320  bitsinv1  13659  bitsinvp1  13666  sadcadd  13675  sadadd2  13677  sadid1  13685  bitsres  13690  smumullem  13709  ressbas  14249  sylow2a  16139  ablfac1eu  16596  indistopon  18627  fctop  18630  cctop  18632  rest0  18795  restsn  18796  filcon  19478  volinun  21049  itg2cnlem2  21262  chtdif  22518  ppidif  22523  ppi1  22524  cht1  22525  0pth  23491  1pthonlem2  23511  disjdifprg  25941  ofpreima2  26007  ordtconlem1  26376  measvuni  26650  measinb  26657  cndprobnul  26842  ballotlemfp1  26896  ballotlemfval0  26900  ballotlemgun  26929  dfpo2  27587  elima4  27612  pred0  27682  mblfinlem2  28455