Theorem vprc 5273

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

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2144  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  nvelOLD  5275  intex  5304  intnex  5305  abnex  7773  iprc  7925  opabn1stprc  8071  elfi2  9411  fi0  9417  ruALT  9608  cardmin2  10085  00lsp  21263  nowisdomv  31082  n0lplig  31092  fveqvfvv  48217  ndmaovcl  48380  vsn  50030  posnex  50201  prsnex  50202