Theorem int0 4800

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 4374	. . . 4 ⊢ ∀𝑥 ∈ ∅ 𝑦 ∈ 𝑥
2		vex 3440	. . . . 5 ⊢ 𝑦 ∈ V
3	2	elint2 4793	. . . 4 ⊢ (𝑦 ∈ ∩ ∅ ↔ ∀𝑥 ∈ ∅ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 232	. . 3 ⊢ 𝑦 ∈ ∩ ∅
5	4, 2	2th 265	. 2 ⊢ (𝑦 ∈ ∩ ∅ ↔ 𝑦 ∈ V)
6	5	eqriv 2792	1 ⊢ ∩ ∅ = V

Syntax hints:   = wceq 1522   ∈ wcel 2081  ∀wral 3105  Vcvv 3437  ∅c0 4215  ∩ cint 4786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-v 3439  df-dif 3866  df-nul 4216  df-int 4787

This theorem is referenced by:  unissint  4810  uniintsn  4823  rint0  4826  intex  5136  intnex  5137  oev2  8004  fiint  8646  elfi2  8729  fi0  8735  cardmin2  9278  00lsp  19448  cmpfi  21705  ptbasfi  21878  fbssint  22135  fclscmp  22327  rankeq1o  33247  bj-0int  34017  heibor1lem  34644