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

Theorem int0 4056
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 3624 . . . . . 6  |-  -.  y  e.  (/)
21pm2.21i 125 . . . . 5  |-  ( y  e.  (/)  ->  x  e.  y )
32ax-gen 1555 . . . 4  |-  A. y
( y  e.  (/)  ->  x  e.  y )
4 equid 1688 . . . 4  |-  x  =  x
53, 42th 231 . . 3  |-  ( A. y ( y  e.  (/)  ->  x  e.  y )  <->  x  =  x
)
65abbii 2547 . 2  |-  { x  |  A. y ( y  e.  (/)  ->  x  e.  y ) }  =  { x  |  x  =  x }
7 df-int 4043 . 2  |-  |^| (/)  =  {
x  |  A. y
( y  e.  (/)  ->  x  e.  y ) }
8 df-v 2950 . 2  |-  _V  =  { x  |  x  =  x }
96, 7, 83eqtr4i 2465 1  |-  |^| (/)  =  _V
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1549    = wceq 1652    e. wcel 1725   {cab 2421   _Vcvv 2948   (/)c0 3620   |^|cint 4042
This theorem is referenced by:  unissint  4066  uniintsn  4079  rint0  4082  intex  4348  intnex  4349  oev2  6758  fiint  7374  elfi2  7410  fi0  7416  cardmin2  7874  00lsp  16045  cmpfi  17459  ptbasfi  17601  fbssint  17858  fclscmp  18050  rankeq1o  26060  heibor1lem  26455
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-dif 3315  df-nul 3621  df-int 4043
  Copyright terms: Public domain W3C validator