Theorem vprc 5260

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.)

Assertion

Ref	Expression
vprc	⊢ ¬ V ∈ V

Proof of Theorem vprc

Step	Hyp	Ref	Expression
1		vnex 5259	. 2 ⊢ ¬ ∃𝑥 𝑥 = V
2		isset 3454	. 2 ⊢ (V ∈ V ↔ ∃𝑥 𝑥 = V)
3	1, 2	mtbir 323	1 ⊢ ¬ V ∈ V

Syntax hints:  ¬ wn 3   = wceq 1541  ∃wex 1780   ∈ wcel 2113  Vcvv 3440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442

This theorem is referenced by:  nvel  5261  intex  5289  intnex  5290  abnex  7702  iprc  7853  opabn1stprc  8002  elfi2  9317  fi0  9323  ruALT  9511  cardmin2  9911  00lsp  20932  n0lplig  30558  fveqvfvv  47286  ndmaovcl  47449  vsn  49057  posnex  49225  prsnex  49226