Theorem int0 4943

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∀wral 3052  Vcvv 3464  ∅c0 4313  ∩ cint 4927

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-v 3466  df-dif 3934  df-nul 4314  df-int 4928

This theorem is referenced by:  unissint  4953  uniintsn  4966  rint0  4969  intex  5319  intnex  5320  oev2  8540  fiint  9343  fiintOLD  9344  elfi2  9431  fi0  9437  cardmin2  10018  00lsp  20943  cmpfi  23351  ptbasfi  23524  fbssint  23781  fclscmp  23973  zarcmplem  33917  rankeq1o  36194  bj-0int  37124  heibor1lem  37838  ipoglb0  48935  mreclat  48938