Theorem in0 3772

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 3747	. . . 4 |- -. x e. (/)
2	1	bianfi 941	. . 3 |- ( x e. (/) <-> ( x e. A /\ x e. (/) ) )
3	2	bicomi 207	. 2 |- ( ( x e. A /\ x e. (/) ) <-> x e. (/) )
4	3	ineqri 3638	1 |- ( A i^i (/) ) = (/)

Syntax hints:   /\ wa 375   = wceq 1455   e. wcel 1898   i^i cin 3415   (/)c0 3743

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-dif 3419  df-in 3423  df-nul 3744

This theorem is referenced by:  csbin  3811  res0  5131  pred0  5433  fresaun  5781  fnsuppeq0  6975  oev2  7256  cda0en  8640  ackbij1lem13  8693  ackbij1lem16  8696  incexclem  13949  bitsinv1  14471  bitsinvp1  14478  sadcadd  14487  sadadd2  14489  sadid1  14497  bitsres  14502  smumullem  14521  ressbas  15234  sylow2a  17326  ablfac1eu  17761  indistopon  20071  fctop  20074  cctop  20076  rest0  20240  restsn  20241  filcon  20953  volinun  22555  itg2cnlem2  22776  chtdif  24141  ppidif  24146  ppi1  24147  cht1  24148  0pth  25356  1pthonlem2  25376  disjdifprg  28239  disjun0  28259  ofpreima2  28321  ordtconlem1  28781  ldgenpisyslem1  29036  measvuni  29087  measinb  29094  0elcarsg  29189  carsgclctunlem1  29199  carsgclctunlem3  29202  cndprobnul  29320  ballotlemfp1  29374  ballotlemfval0  29378  ballotlemgun  29407  ballotlemgunOLD  29445  mrsubvrs  30210  dfpo2  30445  elima4  30471  mblfinlem2  32024  conrel1d  36301  conrel2d  36302  0in  37432  qinioo  37722  nnfoctbdjlem  38398  caragen0  38435  pthdlem2  39890  0pth-av  39937  1pthdlem2  39947