Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  int0 Structured version   Visualization version   GIF version

Theorem int0 4481
 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.
StepHypRef Expression
1 ral0 4067 . . . 4 𝑥 ∈ ∅ 𝑦𝑥
2 vex 3198 . . . . 5 𝑦 ∈ V
32elint2 4473 . . . 4 (𝑦 ∅ ↔ ∀𝑥 ∈ ∅ 𝑦𝑥)
41, 3mpbir 221 . . 3 𝑦
54, 22th 254 . 2 (𝑦 ∅ ↔ 𝑦 ∈ V)
65eqriv 2617 1 ∅ = V
 Colors of variables: wff setvar class Syntax hints:   = wceq 1481   ∈ wcel 1988  ∀wral 2909  Vcvv 3195  ∅c0 3907  ∩ cint 4466 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-v 3197  df-dif 3570  df-nul 3908  df-int 4467 This theorem is referenced by:  unissint  4492  uniintsn  4505  rint0  4508  intex  4811  intnex  4812  oev2  7588  fiint  8222  elfi2  8305  fi0  8311  cardmin2  8809  00lsp  18962  cmpfi  21192  ptbasfi  21365  fbssint  21623  fclscmp  21815  rankeq1o  32253  bj-0int  33030  heibor1lem  33579
 Copyright terms: Public domain W3C validator