Theorem int0 4899

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 4433	. . . 4 ⊢ ∀𝑥 ∈ ∅ 𝑦 ∈ 𝑥
2		vex 3436	. . . . 5 ⊢ 𝑦 ∈ V
3	2	elint2 4891	. . . 4 ⊢ (𝑦 ∈ ∩ ∅ ↔ ∀𝑥 ∈ ∅ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 232	. . 3 ⊢ 𝑦 ∈ ∩ ∅
5	4, 2	2th 265	. 2 ⊢ (𝑦 ∈ ∩ ∅ ↔ 𝑦 ∈ V)
6	5	eqriv 2737	1 ⊢ ∩ ∅ = V

Syntax hints:   = wceq 1547   ∈ wcel 2119  ∀wral 3054  Vcvv 3432  ∅c0 4268  ∩ cint 4884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-v 3434  df-dif 3893  df-nul 4269  df-int 4885

This theorem is referenced by:  unissint  4909  uniintsn  4922  rint0  4925  intex  5279  intnex  5280  oev2  8455  fiint  9234  elfi2  9324  fi0  9330  cardmin2  9921  00lsp  20978  cmpfi  23398  ptbasfi  23571  fbssint  23828  fclscmp  24020  zarcmplem  34072  rankeq1o  36400  bj-0int  37460  heibor1lem  38177  ipoglb0  49485  mreclat  49488