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

Assertion

Ref	Expression
vprc	⊢ ¬ V ∈ V

Proof of Theorem vprc

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

Syntax hints:  ¬ wn 3   = wceq 1540  ∃wex 1779   ∈ wcel 2108  Vcvv 3459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461

This theorem is referenced by:  nvel  5286  intex  5314  intnex  5315  abnex  7749  iprc  7905  opabn1stprc  8055  elfi2  9424  fi0  9430  ruALT  9615  cardmin2  10011  00lsp  20936  n0lplig  30410  fveqvfvv  47017  ndmaovcl  47180  vsn  48738  posnex  48902  prsnex  48903