Theorem vprc 5285

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

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2146  Vcvv 3457

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459

This theorem is used by:  nvelOLD  5287  intex  5316  intnex  5317  abnex  7762  iprc  7914  opabn1stprc  8061  elfi2  9381  fi0  9387  ruALT  9578  cardmin2  10001  00lsp  21152  nowisdomv  30896  n0lplig  30906  fveqvfvv  47835  ndmaovcl  47998  vsn  49647  posnex  49815  prsnex  49816