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

Theorem int0 4415
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 4023 . . . 4 𝑥 ∈ ∅ 𝑦𝑥
2 vex 3171 . . . . 5 𝑦 ∈ V
32elint2 4407 . . . 4 (𝑦 ∅ ↔ ∀𝑥 ∈ ∅ 𝑦𝑥)
41, 3mpbir 219 . . 3 𝑦
54, 22th 252 . 2 (𝑦 ∅ ↔ 𝑦 ∈ V)
65eqriv 2602 1 ∅ = V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wcel 1975  wral 2891  Vcvv 3168  c0 3869   cint 4400
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ral 2896  df-v 3170  df-dif 3538  df-nul 3870  df-int 4401
This theorem is referenced by:  unissint  4426  uniintsn  4439  rint0  4442  intex  4738  intnex  4739  oev2  7463  fiint  8095  elfi2  8176  fi0  8182  cardmin2  8680  00lsp  18744  cmpfi  20959  ptbasfi  21132  fbssint  21390  fclscmp  21582  rankeq1o  31250  heibor1lem  32577
  Copyright terms: Public domain W3C validator