Theorem int0 4914

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  ∀wral 3049  Vcvv 3438  ∅c0 4284  ∩ cint 4899

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3050  df-v 3440  df-dif 3902  df-nul 4285  df-int 4900

This theorem is referenced by:  unissint  4924  uniintsn  4937  rint0  4940  intex  5286  intnex  5287  oev2  8447  fiint  9221  elfi2  9308  fi0  9314  cardmin2  9902  00lsp  20924  cmpfi  23333  ptbasfi  23506  fbssint  23763  fclscmp  23955  zarcmplem  33905  rankeq1o  36226  bj-0int  37156  heibor1lem  37859  ipoglb0  49108  mreclat  49111