MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  int0 Unicode version

Theorem int0 4152
Description: The intersection of the empty set is the universal class. Exercise 2 of [TakeutiZaring] p. 44. (Contributed by NM, 18-Aug-1993.)
Assertion
Ref Expression
int0

Proof of Theorem int0
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 noel 3664 . . . . . 6
21pm2.21i 126 . . . . 5
32ax-gen 1562 . . . 4
4 equid 1698 . . . 4
53, 42th 232 . . 3
65abbii 2593 . 2
7 df-int 4139 . 2
8 df-v 3008 . 2
96, 7, 83eqtr4i 2511 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  A.wal 1556  =wceq 1662  e.wcel 1724  {cab 2467   cvv 3006   c0 3660  |^|cint 4138
This theorem is referenced by:  unissint  4162  uniintsn  4175  rint0  4178  intex  4455  intnex  4456  oev2  6879  fiint  7495  elfi2  7531  fi0  7537  cardmin2  7999  00lsp  16560  cmpfi  17974  ptbasfi  18117  fbssint  18374  fclscmp  18566  rankeq1o  26942  heibor1lem  27381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-v 3008  df-dif 3356  df-nul 3661  df-int 4139
  Copyright terms: Public domain W3C validator