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

Theorem int0 4093
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 3620 . . . . . 6
21pm2.21i 126 . . . . 5
32ax-gen 1556 . . . 4
4 equid 1691 . . . 4
53, 42th 232 . . 3
65abbii 2555 . 2
7 df-int 4080 . 2
8 df-v 2967 . 2
96, 7, 83eqtr4i 2473 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  A.wal 1550  =wceq 1654  e.wcel 1728  {cab 2429   cvv 2965   c0 3616  |^|cint 4079
This theorem is referenced by:  unissint  4103  uniintsn  4116  rint0  4119  intex  4395  intnex  4396  oev2  6816  fiint  7432  elfi2  7468  fi0  7474  cardmin2  7936  00lsp  16108  cmpfi  17522  ptbasfi  17664  fbssint  17921  fclscmp  18113  rankeq1o  26216  heibor1lem  26629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-v 2967  df-dif 3312  df-nul 3617  df-int 4080
  Copyright terms: Public domain W3C validator