Theorem int0 4893

Description: The intersection of the empty set is the universal class. Exercise 2 of [TakeutiZaring] p. 44. (Contributed by NM, 18-Aug-1993.) (Proof shortened by JJ, 26-Jul-2021.)

Assertion

Ref	Expression
int0	⊢ ∩ ∅ = V

Proof of Theorem int0

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ral0 4443	. . . 4 ⊢ ∀𝑥 ∈ ∅ 𝑦 ∈ 𝑥
2		vex 3436	. . . . 5 ⊢ 𝑦 ∈ V
3	2	elint2 4886	. . . 4 ⊢ (𝑦 ∈ ∩ ∅ ↔ ∀𝑥 ∈ ∅ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 230	. . 3 ⊢ 𝑦 ∈ ∩ ∅
5	4, 2	2th 263	. 2 ⊢ (𝑦 ∈ ∩ ∅ ↔ 𝑦 ∈ V)
6	5	eqriv 2735	1 ⊢ ∩ ∅ = V

Syntax hints:   = wceq 1539   ∈ wcel 2106  ∀wral 3064  Vcvv 3432  ∅c0 4256  ∩ cint 4879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-v 3434  df-dif 3890  df-nul 4257  df-int 4880

This theorem is referenced by:  unissint  4903  uniintsn  4918  rint0  4921  intex  5261  intnex  5262  oev2  8353  fiint  9091  elfi2  9173  fi0  9179  cardmin2  9757  00lsp  20243  cmpfi  22559  ptbasfi  22732  fbssint  22989  fclscmp  23181  zarcmplem  31831  rankeq1o  34473  bj-0int  35272  heibor1lem  35967  ipoglb0  46280  mreclat  46283