Theorem int0 3446

Description: The intersection of the empty set is the universal class. Exercise 2 of [TakeutiZaring] p. 44.

Assertion

Ref	Expression
int0	|- |^|(/) = _V

Proof of Theorem int0

Step	Hyp	Ref	Expression
1		noel 3118	. . . . . 6 |- -. y e. (/)
2	1	pm2.21i 130	. . . . 5 |- (y e. (/) -> x e. y)
3	2	ax-gen 1622	. . . 4 |- A.y(y e. (/) -> x e. y)
4		eqid 2170	. . . 4 |- x = x
5	3, 4	2th 292	. . 3 |- (A.y(y e. (/) -> x e. y) <-> x = x)
6	5	abbii 2284	. 2 |- {x | A.y(y e. (/) -> x e. y)} = {x | x = x}
7		df-int 3433	. 2 |- |^|(/) = {x | A.y(y e. (/) -> x e. y)}
8		df-v 2571	. 2 |- _V = {x | x = x}
9	6, 7, 8	3eqtr4i 2200	1 |- |^|(/) = _V

Syntax hints:   -> wi 3  A.wal 1613   = wceq 1615   e. wcel 1617  {cab 2157  _Vcvv 2569  (/)c0 3114  |^|cint 3432

This theorem is referenced by:  unissint 3455  uniintsn 3466  intex 3664  intnex 3665  oev2 5413  fiint 5916  cardval3 6169  cardmin2 6203  fiuni 11212  fiiu2 11213  fbssint 11275  fsubbas 11277  fiiu 15313  efilcp 15949  efilcp2 15953  cnfilca 15954  elfiun 16454  compfipin0 16521  fbasfip 16641  fcluscomplem 16705  fcluscomp 16706  inficl 16842  heiborlem13 17052

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-ex 1645  df-sb 1845  df-clab 2158  df-cleq 2163  df-clel 2166  df-v 2571  df-dif 2862  df-nul 3115  df-int 3433

Copyright terms: Public domain