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

Theorem vprc 5315
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 5314 . 2 ¬ ∃𝑥 𝑥 = V
2 isset 3494 . 2 (V ∈ V ↔ ∃𝑥 𝑥 = V)
31, 2mtbir 323 1 ¬ V ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1540  wex 1779  wcel 2108  Vcvv 3480
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  ax-sep 5296
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482
This theorem is referenced by:  nvel  5316  intex  5344  intnex  5345  abnex  7777  iprc  7933  opabn1stprc  8083  elfi2  9454  fi0  9460  ruALT  9643  cardmin2  10039  00lsp  20979  n0lplig  30502  fveqvfvv  47052  ndmaovcl  47215  vsn  48731
  Copyright terms: Public domain W3C validator