Theorem int0 4986

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

Syntax hints:   = wceq 1537   ∈ wcel 2108  ∀wral 3067  Vcvv 3488  ∅c0 4352  ∩ cint 4970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-v 3490  df-dif 3979  df-nul 4353  df-int 4971

This theorem is referenced by:  unissint  4996  uniintsn  5009  rint0  5012  intex  5362  intnex  5363  oev2  8579  fiint  9394  fiintOLD  9395  elfi2  9483  fi0  9489  cardmin2  10068  00lsp  21002  cmpfi  23437  ptbasfi  23610  fbssint  23867  fclscmp  24059  zarcmplem  33827  rankeq1o  36135  bj-0int  37067  heibor1lem  37769  ipoglb0  48666  mreclat  48669