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

Theorem int0 3892
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 3472 . . . . . 6  |-  -.  y  e.  (/)
21pm2.21i 123 . . . . 5  |-  ( y  e.  (/)  ->  x  e.  y )
32ax-gen 1536 . . . 4  |-  A. y
( y  e.  (/)  ->  x  e.  y )
4 eqid 2296 . . . 4  |-  x  =  x
53, 42th 230 . . 3  |-  ( A. y ( y  e.  (/)  ->  x  e.  y )  <->  x  =  x
)
65abbii 2408 . 2  |-  { x  |  A. y ( y  e.  (/)  ->  x  e.  y ) }  =  { x  |  x  =  x }
7 df-int 3879 . 2  |-  |^| (/)  =  {
x  |  A. y
( y  e.  (/)  ->  x  e.  y ) }
8 df-v 2803 . 2  |-  _V  =  { x  |  x  =  x }
96, 7, 83eqtr4i 2326 1  |-  |^| (/)  =  _V
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530    = wceq 1632    e. wcel 1696   {cab 2282   _Vcvv 2801   (/)c0 3468   |^|cint 3878
This theorem is referenced by:  unissint  3902  uniintsn  3915  rint0  3918  intex  4183  intnex  4184  oev2  6538  fiint  7149  elfi2  7184  fi0  7189  cardmin2  7647  incexclem  12311  incexc  12312  00lsp  15754  cmpfi  17151  ptbasfi  17292  fbssint  17549  fclscmp  17741  rankeq1o  24873  heibor1lem  26636
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-dif 3168  df-nul 3469  df-int 3879
  Copyright terms: Public domain W3C validator