Theorem int0 4915

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 4466	. . . 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 2726	1 ⊢ ∩ ∅ = V

Syntax hints:   = wceq 1540   ∈ wcel 2109  ∀wral 3044  Vcvv 3438  ∅c0 4286  ∩ cint 4899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3440  df-dif 3908  df-nul 4287  df-int 4900

This theorem is referenced by:  unissint  4925  uniintsn  4938  rint0  4941  intex  5286  intnex  5287  oev2  8448  fiint  9235  fiintOLD  9236  elfi2  9323  fi0  9329  cardmin2  9914  00lsp  20902  cmpfi  23311  ptbasfi  23484  fbssint  23741  fclscmp  23933  zarcmplem  33847  rankeq1o  36144  bj-0int  37074  heibor1lem  37788  ipoglb0  48966  mreclat  48969