Theorem vprc 5255

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

Syntax hints:  ¬ wn 3   ∈ wcel 2114  Vcvv 3429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431

This theorem is referenced by:  nvelOLD  5257  intex  5285  intnex  5286  abnex  7711  iprc  7862  opabn1stprc  8011  elfi2  9327  fi0  9333  ruALT  9523  cardmin2  9923  00lsp  20976  nowisdomv  30544  n0lplig  30554  fveqvfvv  47488  ndmaovcl  47651  vsn  49287  posnex  49455  prsnex  49456