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

Proof of Theorem in0

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		noel 3788	. . . 4
2	1	bianfi 925	. . 3
3	2	bicomi 202	. 2
4	3	ineqri 3691	1

Syntax hints:  /\wa 369  =wceq 1395  e.wcel 1818  i^icin 3474  c0 3784

This theorem is referenced by:  csbin  3860  res0  5283  fresaun  5761  fnsuppeq0OLD  6132  fnsuppeq0  6947  oev2  7192  cda0en  8580  ackbij1lem13  8633  ackbij1lem16  8636  incexclem  13648  bitsinv1  14092  bitsinvp1  14099  sadcadd  14108  sadadd2  14110  sadid1  14118  bitsres  14123  smumullem  14142  ressbas  14687  sylow2a  16639  ablfac1eu  17124  indistopon  19502  fctop  19505  cctop  19507  rest0  19670  restsn  19671  filcon  20384  volinun  21956  itg2cnlem2  22169  chtdif  23432  ppidif  23437  ppi1  23438  cht1  23439  0pth  24572  1pthonlem2  24592  disjdifprg  27436  ofpreima2  27508  ordtconlem1  27906  measvuni  28185  measinb  28192  cndprobnul  28376  ballotlemfp1  28430  ballotlemfval0  28434  ballotlemgun  28463  mrsubvrs  28882  dfpo2  29184  elima4  29209  pred0  29279  mblfinlem2  30052  conrel1d  37761  conrel2d  37762

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-in 3482  df-nul 3785