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

Theorem int0 4924
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 4471 . . . 4 𝑥 ∈ ∅ 𝑦𝑥
2 vex 3448 . . . . 5 𝑦 ∈ V
32elint2 4915 . . . 4 (𝑦 ∅ ↔ ∀𝑥 ∈ ∅ 𝑦𝑥)
41, 3mpbir 230 . . 3 𝑦
54, 22th 264 . 2 (𝑦 ∅ ↔ 𝑦 ∈ V)
65eqriv 2730 1 ∅ = V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  wcel 2107  wral 3061  Vcvv 3444  c0 4283   cint 4908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-v 3446  df-dif 3914  df-nul 4284  df-int 4909
This theorem is referenced by:  unissint  4934  uniintsn  4949  rint0  4952  intex  5295  intnex  5296  oev2  8470  fiint  9271  elfi2  9355  fi0  9361  cardmin2  9940  00lsp  20457  cmpfi  22775  ptbasfi  22948  fbssint  23205  fclscmp  23397  zarcmplem  32519  rankeq1o  34802  bj-0int  35618  heibor1lem  36314  ipoglb0  47105  mreclat  47108
  Copyright terms: Public domain W3C validator