Theorem int0 4490

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 4076	. . . 4 ⊢ ∀𝑥 ∈ ∅ 𝑦 ∈ 𝑥
2		vex 3203	. . . . 5 ⊢ 𝑦 ∈ V
3	2	elint2 4482	. . . 4 ⊢ (𝑦 ∈ ∩ ∅ ↔ ∀𝑥 ∈ ∅ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 221	. . 3 ⊢ 𝑦 ∈ ∩ ∅
5	4, 2	2th 254	. 2 ⊢ (𝑦 ∈ ∩ ∅ ↔ 𝑦 ∈ V)
6	5	eqriv 2619	1 ⊢ ∩ ∅ = V

Syntax hints:   = wceq 1483   ∈ wcel 1990  ∀wral 2912  Vcvv 3200  ∅c0 3915  ∩ cint 4475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202  df-dif 3577  df-nul 3916  df-int 4476

This theorem is referenced by:  unissint  4501  uniintsn  4514  rint0  4517  intex  4820  intnex  4821  oev2  7603  fiint  8237  elfi2  8320  fi0  8326  cardmin2  8824  00lsp  18981  cmpfi  21211  ptbasfi  21384  fbssint  21642  fclscmp  21834  rankeq1o  32278  bj-0int  33055  heibor1lem  33608