Theorem int0 4925

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  ∀wral 3078  Vcvv 3453  ∅c0 4282  ∩ cint 4910

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-v 3455  df-dif 3905  df-nul 4283  df-int 4911

This theorem is used by:  unissint  4935  uniintsn  4948  rint0  4951  intex  5312  intnex  5313  oev2  8513  fiint  9299  elfi2  9387  fi0  9393  cardmin2  10007  00lsp  21169  cmpfi  23637  ptbasfi  23811  fbssint  24068  fclscmp  24260  zarcmplem  34393  rankeq1o  36753  bj-0int  37853  heibor1lem  38561  ipoglb0  49922  mreclat  49925