Theorem vprc 5282

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 5281	1 ⊢ ¬ V ∈ V

Syntax hints:  ¬ wn 3   ∈ wcel 2149  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465

This theorem is referenced by:  nvelOLD  5284  intex  5312  intnex  5313  abnex  7752  iprc  7904  opabn1stprc  8051  elfi2  9370  fi0  9376  ruALT  9567  cardmin2  9981  00lsp  21076  nowisdomv  30762  n0lplig  30772  fveqvfvv  47661  ndmaovcl  47824  vsn  49470  posnex  49638  prsnex  49639