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

Theorem int0 4241
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 3742 . . . . . 6  |-  -.  y  e.  (/)
21pm2.21i 131 . . . . 5  |-  ( y  e.  (/)  ->  x  e.  y )
32ax-gen 1639 . . . 4  |-  A. y
( y  e.  (/)  ->  x  e.  y )
4 equid 1815 . . . 4  |-  x  =  x
53, 42th 239 . . 3  |-  ( A. y ( y  e.  (/)  ->  x  e.  y )  <->  x  =  x
)
65abbii 2536 . 2  |-  { x  |  A. y ( y  e.  (/)  ->  x  e.  y ) }  =  { x  |  x  =  x }
7 df-int 4228 . 2  |-  |^| (/)  =  {
x  |  A. y
( y  e.  (/)  ->  x  e.  y ) }
8 df-v 3061 . 2  |-  _V  =  { x  |  x  =  x }
96, 7, 83eqtr4i 2441 1  |-  |^| (/)  =  _V
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1403    = wceq 1405    e. wcel 1842   {cab 2387   _Vcvv 3059   (/)c0 3738   |^|cint 4227
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3061  df-dif 3417  df-nul 3739  df-int 4228
This theorem is referenced by:  unissint  4252  uniintsn  4265  rint0  4268  intex  4550  intnex  4551  oev2  7210  fiint  7831  elfi2  7908  fi0  7914  cardmin2  8411  00lsp  17947  cmpfi  20201  ptbasfi  20374  fbssint  20631  fclscmp  20823  rankeq1o  30509  heibor1lem  31587
  Copyright terms: Public domain W3C validator