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

Theorem int0 4242
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 3741 . . . . . 6  |-  -.  y  e.  (/)
21pm2.21i 131 . . . . 5  |-  ( y  e.  (/)  ->  x  e.  y )
32ax-gen 1592 . . . 4  |-  A. y
( y  e.  (/)  ->  x  e.  y )
4 equid 1731 . . . 4  |-  x  =  x
53, 42th 239 . . 3  |-  ( A. y ( y  e.  (/)  ->  x  e.  y )  <->  x  =  x
)
65abbii 2585 . 2  |-  { x  |  A. y ( y  e.  (/)  ->  x  e.  y ) }  =  { x  |  x  =  x }
7 df-int 4229 . 2  |-  |^| (/)  =  {
x  |  A. y
( y  e.  (/)  ->  x  e.  y ) }
8 df-v 3072 . 2  |-  _V  =  { x  |  x  =  x }
96, 7, 83eqtr4i 2490 1  |-  |^| (/)  =  _V
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1368    = wceq 1370    e. wcel 1758   {cab 2436   _Vcvv 3070   (/)c0 3737   |^|cint 4228
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3072  df-dif 3431  df-nul 3738  df-int 4229
This theorem is referenced by:  unissint  4252  uniintsn  4265  rint0  4268  intex  4548  intnex  4549  oev2  7065  fiint  7691  elfi2  7767  fi0  7773  cardmin2  8271  00lsp  17170  cmpfi  19129  ptbasfi  19272  fbssint  19529  fclscmp  19721  rankeq1o  28345  heibor1lem  28848
  Copyright terms: Public domain W3C validator