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

Theorem int0 4168
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 3677 . . . . . 6
21pm2.21i 126 . . . . 5
32ax-gen 1570 . . . 4
4 equid 1706 . . . 4
53, 42th 232 . . 3
65abbii 2601 . 2
7 df-int 4155 . 2
8 df-v 3017 . 2
96, 7, 83eqtr4i 2519 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  A.wal 1564  =wceq 1670  e.wcel 1732  {cab 2475   cvv 3015   c0 3673  |^|cint 4154
This theorem is referenced by:  unissint  4178  uniintsn  4191  rint0  4194  intex  4471  intnex  4472  oev2  6929  fiint  7549  elfi2  7586  fi0  7592  cardmin2  8054  00lsp  16676  cmpfi  18485  ptbasfi  18628  fbssint  18885  fclscmp  19077  rankeq1o  27451  heibor1lem  27890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-v 3017  df-dif 3368  df-nul 3674  df-int 4155
  Copyright terms: Public domain W3C validator