Theorem int0 4926

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 4476	. . . 4 ⊢ ∀𝑥 ∈ ∅ 𝑦 ∈ 𝑥
2		vex 3451	. . . . 5 ⊢ 𝑦 ∈ V
3	2	elint2 4917	. . . 4 ⊢ (𝑦 ∈ ∩ ∅ ↔ ∀𝑥 ∈ ∅ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 231	. . 3 ⊢ 𝑦 ∈ ∩ ∅
5	4, 2	2th 264	. 2 ⊢ (𝑦 ∈ ∩ ∅ ↔ 𝑦 ∈ V)
6	5	eqriv 2726	1 ⊢ ∩ ∅ = V

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∀wral 3044  Vcvv 3447  ∅c0 4296  ∩ cint 4910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3449  df-dif 3917  df-nul 4297  df-int 4911

This theorem is referenced by:  unissint  4936  uniintsn  4949  rint0  4952  intex  5299  intnex  5300  oev2  8487  fiint  9277  fiintOLD  9278  elfi2  9365  fi0  9371  cardmin2  9952  00lsp  20887  cmpfi  23295  ptbasfi  23468  fbssint  23725  fclscmp  23917  zarcmplem  33871  rankeq1o  36159  bj-0int  37089  heibor1lem  37803  ipoglb0  48982  mreclat  48985