Theorem vprc 5283

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.) (Proof shortened by BJ, 1-May-2026.)

Assertion

Ref	Expression
vprc	⊢ ¬ V ∈ V

Proof of Theorem vprc

Step	Hyp	Ref	Expression
1		nvel 5282	1 ⊢ ¬ V ∈ V

Syntax hints:  ¬ wn 3   ∈ wcel 2143  Vcvv 3455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457

This theorem is referenced by:  nvelOLD  5285  intex  5314  intnex  5315  abnex  7752  iprc  7904  opabn1stprc  8051  elfi2  9370  fi0  9376  ruALT  9567  cardmin2  9981  00lsp  21102  nowisdomv  30825  n0lplig  30835  fveqvfvv  47777  ndmaovcl  47940  vsn  49590  posnex  49758  prsnex  49759