Theorem vprc 5277

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

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

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 2732  ax-sep 5251

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  nvelOLD  5279  intex  5308  intnex  5309  abnex  7756  iprc  7908  opabn1stprc  8055  elfi2  9384  fi0  9390  ruALT  9581  cardmin2  10004  00lsp  21165  nowisdomv  30954  n0lplig  30964  fveqvfvv  47928  ndmaovcl  48091  vsn  49740  posnex  49906  prsnex  49907