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

Theorem vprc 5320
Description: The universal class is not a member of itself (and thus is not a set). Proposition 5.21 of [TakeutiZaring] p. 21; our proof, however, does not depend on the Axiom of Regularity. (Contributed by NM, 23-Aug-1993.)
Assertion
Ref Expression
vprc ¬ V ∈ V

Proof of Theorem vprc
StepHypRef Expression
1 vnex 5319 . 2 ¬ ∃𝑥 𝑥 = V
2 isset 3491 . 2 (V ∈ V ↔ ∃𝑥 𝑥 = V)
31, 2mtbir 323 1 ¬ V ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1536  wex 1775  wcel 2105  Vcvv 3477
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479
This theorem is referenced by:  nvel  5321  intex  5349  intnex  5350  abnex  7775  iprc  7933  opabn1stprc  8081  elfi2  9451  fi0  9457  ruALT  9640  cardmin2  10036  00lsp  20996  n0lplig  30511  fveqvfvv  46989  ndmaovcl  47152  vsn  48659
  Copyright terms: Public domain W3C validator