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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  ∀wral 3080  Vcvv 3454  ∅c0 4281  ∩ 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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-v 3456  df-dif 4050  df-nul 4282  df-int 4911

This theorem is used by:  unissint  4935  uniintsn  4948  rint0  4951  intex  5309  intnex  5310  oev2  8559  fiint  9346  elfi2  9433  fi0  9439  cardmin2  10107  00lsp  21286  cmpfi  23756  ptbasfi  23930  fbssint  24187  fclscmp  24379  zarcmplem  34583  rankeq1o  37110  bj-0int  38213  heibor1lem  38935  ipoglb0  50313  mreclat  50316