Theorem vprc 5257

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 5256	. 2 ⊢ ¬ ∃𝑥 𝑥 = V
2		isset 3451	. 2 ⊢ (V ∈ V ↔ ∃𝑥 𝑥 = V)
3	1, 2	mtbir 323	1 ⊢ ¬ V ∈ V

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

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 2705  ax-sep 5238

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439

This theorem is referenced by:  nvel  5258  intex  5286  intnex  5287  abnex  7699  iprc  7850  opabn1stprc  7999  elfi2  9309  fi0  9315  ruALT  9503  cardmin2  9903  00lsp  20923  n0lplig  30484  fveqvfvv  47202  ndmaovcl  47365  vsn  48973  posnex  49141  prsnex  49142