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

Theorem int0 4066
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  |-  |^| (/)  =  _V

Proof of Theorem int0
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 noel 3634 . . . . . 6  |-  -.  y  e.  (/)
21pm2.21i 126 . . . . 5  |-  ( y  e.  (/)  ->  x  e.  y )
32ax-gen 1556 . . . 4  |-  A. y
( y  e.  (/)  ->  x  e.  y )
4 equid 1689 . . . 4  |-  x  =  x
53, 42th 232 . . 3  |-  ( A. y ( y  e.  (/)  ->  x  e.  y )  <->  x  =  x
)
65abbii 2550 . 2  |-  { x  |  A. y ( y  e.  (/)  ->  x  e.  y ) }  =  { x  |  x  =  x }
7 df-int 4053 . 2  |-  |^| (/)  =  {
x  |  A. y
( y  e.  (/)  ->  x  e.  y ) }
8 df-v 2960 . 2  |-  _V  =  { x  |  x  =  x }
96, 7, 83eqtr4i 2468 1  |-  |^| (/)  =  _V
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1550    = wceq 1653    e. wcel 1726   {cab 2424   _Vcvv 2958   (/)c0 3630   |^|cint 4052
This theorem is referenced by:  unissint  4076  uniintsn  4089  rint0  4092  intex  4358  intnex  4359  oev2  6769  fiint  7385  elfi2  7421  fi0  7427  cardmin2  7887  00lsp  16059  cmpfi  17473  ptbasfi  17615  fbssint  17872  fclscmp  18064  rankeq1o  26114  heibor1lem  26520
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
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 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-dif 3325  df-nul 3631  df-int 4053
  Copyright terms: Public domain W3C validator