Theorem int0 4923

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 4455	. . . 4 ⊢ ∀𝑥 ∈ ∅ 𝑦 ∈ 𝑥
2		vex 3461	. . . . 5 ⊢ 𝑦 ∈ V
3	2	elint2 4915	. . . 4 ⊢ (𝑦 ∈ ∩ ∅ ↔ ∀𝑥 ∈ ∅ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 234	. . 3 ⊢ 𝑦 ∈ ∩ ∅
5	4, 2	2th 267	. 2 ⊢ (𝑦 ∈ ∩ ∅ ↔ 𝑦 ∈ V)
6	5	eqriv 2762	1 ⊢ ∩ ∅ = V

Syntax hints:   = wceq 1563   ∈ wcel 2145  ∀wral 3079  Vcvv 3457  ∅c0 4288  ∩ cint 4908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-v 3459  df-dif 3910  df-nul 4289  df-int 4909

This theorem is referenced by:  unissint  4933  uniintsn  4946  rint0  4949  intex  5305  intnex  5306  oev2  8496  fiint  9274  elfi2  9362  fi0  9368  cardmin2  9973  00lsp  21071  cmpfi  23526  ptbasfi  23699  fbssint  23956  fclscmp  24148  zarcmplem  34188  rankeq1o  36534  bj-0int  37603  heibor1lem  38320  ipoglb0  49623  mreclat  49626