Theorem int0 4910

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

Syntax hints:   = wceq 1541   ∈ wcel 2110  ∀wral 3045  Vcvv 3434  ∅c0 4281  ∩ cint 4895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-v 3436  df-dif 3903  df-nul 4282  df-int 4896

This theorem is referenced by:  unissint  4920  uniintsn  4933  rint0  4936  intex  5280  intnex  5281  oev2  8433  fiint  9206  elfi2  9293  fi0  9299  cardmin2  9884  00lsp  20907  cmpfi  23316  ptbasfi  23489  fbssint  23746  fclscmp  23938  zarcmplem  33884  rankeq1o  36184  bj-0int  37114  heibor1lem  37828  ipoglb0  49004  mreclat  49007