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

Theorem int0 3877
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
StepHypRef Expression
1 noel 3460 . . . . . 6  |-  -.  y  e.  (/)
21pm2.21i 125 . . . . 5  |-  ( y  e.  (/)  ->  x  e.  y )
32ax-gen 1538 . . . 4  |-  A. y
( y  e.  (/)  ->  x  e.  y )
4 eqid 2284 . . . 4  |-  x  =  x
53, 42th 232 . . 3  |-  ( A. y ( y  e.  (/)  ->  x  e.  y )  <->  x  =  x
)
65abbii 2396 . 2  |-  { x  |  A. y ( y  e.  (/)  ->  x  e.  y ) }  =  { x  |  x  =  x }
7 df-int 3864 . 2  |-  |^| (/)  =  {
x  |  A. y
( y  e.  (/)  ->  x  e.  y ) }
8 df-v 2791 . 2  |-  _V  =  { x  |  x  =  x }
96, 7, 83eqtr4i 2314 1  |-  |^| (/)  =  _V
Colors of variables: wff set class
Syntax hints:    -> wi 6   A.wal 1532    = wceq 1628    e. wcel 1688   {cab 2270   _Vcvv 2789   (/)c0 3456   |^|cint 3863
This theorem is referenced by:  unissint  3887  uniintsn  3900  rint0  3903  intex  4170  intnex  4171  oev2  6517  fiint  7128  elfi2  7163  fi0  7168  cardmin2  7626  incexclem  12289  incexc  12290  00lsp  15732  cmpfi  17129  ptbasfi  17270  fbssint  17527  fclscmp  17719  rankeq1o  24208  heibor1lem  25932
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-dif 3156  df-nul 3457  df-int 3864
  Copyright terms: Public domain W3C validator