Theorem int0 4890

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 4440	. . . 4 ⊢ ∀𝑥 ∈ ∅ 𝑦 ∈ 𝑥
2		vex 3426	. . . . 5 ⊢ 𝑦 ∈ V
3	2	elint2 4883	. . . 4 ⊢ (𝑦 ∈ ∩ ∅ ↔ ∀𝑥 ∈ ∅ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 230	. . 3 ⊢ 𝑦 ∈ ∩ ∅
5	4, 2	2th 263	. 2 ⊢ (𝑦 ∈ ∩ ∅ ↔ 𝑦 ∈ V)
6	5	eqriv 2735	1 ⊢ ∩ ∅ = V

Syntax hints:   = wceq 1539   ∈ wcel 2108  ∀wral 3063  Vcvv 3422  ∅c0 4253  ∩ cint 4876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-v 3424  df-dif 3886  df-nul 4254  df-int 4877

This theorem is referenced by:  unissint  4900  uniintsn  4915  rint0  4918  intex  5256  intnex  5257  oev2  8315  fiint  9021  elfi2  9103  fi0  9109  cardmin2  9688  00lsp  20158  cmpfi  22467  ptbasfi  22640  fbssint  22897  fclscmp  23089  zarcmplem  31733  rankeq1o  34400  bj-0int  35199  heibor1lem  35894  ipoglb0  46168  mreclat  46171