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

Theorem int0 4962
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 4513 . . . 4 𝑥 ∈ ∅ 𝑦𝑥
2 vex 3484 . . . . 5 𝑦 ∈ V
32elint2 4953 . . . 4 (𝑦 ∅ ↔ ∀𝑥 ∈ ∅ 𝑦𝑥)
41, 3mpbir 231 . . 3 𝑦
54, 22th 264 . 2 (𝑦 ∅ ↔ 𝑦 ∈ V)
65eqriv 2734 1 ∅ = V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  wcel 2108  wral 3061  Vcvv 3480  c0 4333   cint 4946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-v 3482  df-dif 3954  df-nul 4334  df-int 4947
This theorem is referenced by:  unissint  4972  uniintsn  4985  rint0  4988  intex  5344  intnex  5345  oev2  8561  fiint  9366  fiintOLD  9367  elfi2  9454  fi0  9460  cardmin2  10039  00lsp  20979  cmpfi  23416  ptbasfi  23589  fbssint  23846  fclscmp  24038  zarcmplem  33880  rankeq1o  36172  bj-0int  37102  heibor1lem  37816  ipoglb0  48883  mreclat  48886
  Copyright terms: Public domain W3C validator