Theorem vprc 5274

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

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2145  Vcvv 3451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453

This theorem is used by:  nvelOLD  5276  intex  5305  intnex  5306  abnex  7772  iprc  7924  opabn1stprc  8070  elfi2  9407  fi0  9413  ruALT  9604  cardmin2  10081  00lsp  21257  nowisdomv  31076  n0lplig  31086  fveqvfvv  48111  ndmaovcl  48274  vsn  49923  posnex  50089  prsnex  50090