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

Theorem int0 4289
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 3782 . . . . . 6  |-  -.  y  e.  (/)
21pm2.21i 131 . . . . 5  |-  ( y  e.  (/)  ->  x  e.  y )
32ax-gen 1596 . . . 4  |-  A. y
( y  e.  (/)  ->  x  e.  y )
4 equid 1735 . . . 4  |-  x  =  x
53, 42th 239 . . 3  |-  ( A. y ( y  e.  (/)  ->  x  e.  y )  <->  x  =  x
)
65abbii 2594 . 2  |-  { x  |  A. y ( y  e.  (/)  ->  x  e.  y ) }  =  { x  |  x  =  x }
7 df-int 4276 . 2  |-  |^| (/)  =  {
x  |  A. y
( y  e.  (/)  ->  x  e.  y ) }
8 df-v 3108 . 2  |-  _V  =  { x  |  x  =  x }
96, 7, 83eqtr4i 2499 1  |-  |^| (/)  =  _V
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1372    = wceq 1374    e. wcel 1762   {cab 2445   _Vcvv 3106   (/)c0 3778   |^|cint 4275
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-dif 3472  df-nul 3779  df-int 4276
This theorem is referenced by:  unissint  4299  uniintsn  4312  rint0  4315  intex  4596  intnex  4597  oev2  7163  fiint  7786  elfi2  7863  fi0  7869  cardmin2  8368  00lsp  17403  cmpfi  19667  ptbasfi  19810  fbssint  20067  fclscmp  20259  rankeq1o  29255  heibor1lem  29759
  Copyright terms: Public domain W3C validator