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

Theorem vprc 5273
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 5272 . 2 ¬ ∃𝑥 𝑥 = V
2 isset 3459 . 2 (V ∈ V ↔ ∃𝑥 𝑥 = V)
31, 2mtbir 323 1 ¬ V ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1542  wex 1782  wcel 2107  Vcvv 3446
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 2708  ax-sep 5257
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448
This theorem is referenced by:  nvel  5274  intex  5295  intnex  5296  abnex  7692  iprc  7851  opabn1stprc  7991  elfi2  9351  fi0  9357  ruALT  9540  cardmin2  9936  00lsp  20445  n0lplig  29428  fveqvfvv  45281  ndmaovcl  45442  vsn  46903
  Copyright terms: Public domain W3C validator