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

Theorem int0 4643
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 4221 . . . 4 𝑥 ∈ ∅ 𝑦𝑥
2 vex 3344 . . . . 5 𝑦 ∈ V
32elint2 4635 . . . 4 (𝑦 ∅ ↔ ∀𝑥 ∈ ∅ 𝑦𝑥)
41, 3mpbir 221 . . 3 𝑦
54, 22th 254 . 2 (𝑦 ∅ ↔ 𝑦 ∈ V)
65eqriv 2758 1 ∅ = V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  wcel 2140  wral 3051  Vcvv 3341  c0 4059   cint 4628
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-ral 3056  df-v 3343  df-dif 3719  df-nul 4060  df-int 4629
This theorem is referenced by:  unissint  4654  uniintsn  4667  rint0  4670  intex  4970  intnex  4971  oev2  7775  fiint  8405  elfi2  8488  fi0  8494  cardmin2  9035  00lsp  19204  cmpfi  21434  ptbasfi  21607  fbssint  21864  fclscmp  22056  rankeq1o  32606  bj-0int  33380  heibor1lem  33940
  Copyright terms: Public domain W3C validator