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  7769  iprc  7921  opabn1stprc  8067  elfi2  9399  fi0  9405  ruALT  9596  cardmin2  10073  00lsp  21249  nowisdomv  31068  n0lplig  31078  fveqvfvv  48079  ndmaovcl  48242  vsn  49891  posnex  50057  prsnex  50058