Theorem int0 4914

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 4446	. . . 4 ⊢ ∀𝑥 ∈ ∅ 𝑦 ∈ 𝑥
2		vex 3452	. . . . 5 ⊢ 𝑦 ∈ V
3	2	elint2 4906	. . . 4 ⊢ (𝑦 ∈ ∩ ∅ ↔ ∀𝑥 ∈ ∅ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 233	. . 3 ⊢ 𝑦 ∈ ∩ ∅
5	4, 2	2th 266	. 2 ⊢ (𝑦 ∈ ∩ ∅ ↔ 𝑦 ∈ V)
6	5	eqriv 2753	1 ⊢ ∩ ∅ = V

Syntax hints:   = wceq 1554   ∈ wcel 2136  ∀wral 3070  Vcvv 3448  ∅c0 4280  ∩ cint 4899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-ral 3071  df-v 3450  df-dif 3902  df-nul 4281  df-int 4900

This theorem is referenced by:  unissint  4924  uniintsn  4937  rint0  4940  intex  5294  intnex  5295  oev2  8480  fiint  9260  elfi2  9350  fi0  9356  cardmin2  9947  00lsp  21021  cmpfi  23441  ptbasfi  23614  fbssint  23871  fclscmp  24063  zarcmplem  34132  rankeq1o  36469  bj-0int  37539  heibor1lem  38256  ipoglb0  49563  mreclat  49566