Theorem int0 4929

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∀wral 3045  Vcvv 3450  ∅c0 4299  ∩ cint 4913

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-v 3452  df-dif 3920  df-nul 4300  df-int 4914

This theorem is referenced by:  unissint  4939  uniintsn  4952  rint0  4955  intex  5302  intnex  5303  oev2  8490  fiint  9284  fiintOLD  9285  elfi2  9372  fi0  9378  cardmin2  9959  00lsp  20894  cmpfi  23302  ptbasfi  23475  fbssint  23732  fclscmp  23924  zarcmplem  33878  rankeq1o  36166  bj-0int  37096  heibor1lem  37810  ipoglb0  48986  mreclat  48989