Theorem int0 4942

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

Syntax hints:   = wceq 1539   ∈ wcel 2107  ∀wral 3050  Vcvv 3463  ∅c0 4313  ∩ cint 4926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-v 3465  df-dif 3934  df-nul 4314  df-int 4927

This theorem is referenced by:  unissint  4952  uniintsn  4965  rint0  4968  intex  5324  intnex  5325  oev2  8543  fiint  9348  fiintOLD  9349  elfi2  9436  fi0  9442  cardmin2  10021  00lsp  20948  cmpfi  23363  ptbasfi  23536  fbssint  23793  fclscmp  23985  zarcmplem  33855  rankeq1o  36147  bj-0int  37077  heibor1lem  37791  ipoglb0  48875  mreclat  48878