Theorem int0 4962

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  ∀wral 3061  Vcvv 3480  ∅c0 4333  ∩ cint 4946

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-v 3482  df-dif 3954  df-nul 4334  df-int 4947

This theorem is referenced by:  unissint  4972  uniintsn  4985  rint0  4988  intex  5344  intnex  5345  oev2  8561  fiint  9366  fiintOLD  9367  elfi2  9454  fi0  9460  cardmin2  10039  00lsp  20979  cmpfi  23416  ptbasfi  23589  fbssint  23846  fclscmp  24038  zarcmplem  33880  rankeq1o  36172  bj-0int  37102  heibor1lem  37816  ipoglb0  48883  mreclat  48886