Theorem vprc 5242

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

Syntax hints:  ¬ wn 3   ∈ wcel 2119  Vcvv 3431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433

This theorem is referenced by:  nvelOLD  5244  intex  5272  intnex  5273  abnex  7700  iprc  7851  opabn1stprc  8000  elfi2  9317  fi0  9323  ruALT  9514  cardmin2  9914  00lsp  20971  nowisdomv  30562  n0lplig  30572  fveqvfvv  47503  ndmaovcl  47666  vsn  49302  posnex  49470  prsnex  49471