Theorem int0 4967

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

Syntax hints:   = wceq 1537   ∈ wcel 2106  ∀wral 3059  Vcvv 3478  ∅c0 4339  ∩ cint 4951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-v 3480  df-dif 3966  df-nul 4340  df-int 4952

This theorem is referenced by:  unissint  4977  uniintsn  4990  rint0  4993  intex  5350  intnex  5351  oev2  8560  fiint  9364  fiintOLD  9365  elfi2  9452  fi0  9458  cardmin2  10037  00lsp  20997  cmpfi  23432  ptbasfi  23605  fbssint  23862  fclscmp  24054  zarcmplem  33842  rankeq1o  36153  bj-0int  37084  heibor1lem  37796  ipoglb0  48783  mreclat  48786