Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  vprc Structured version   Visualization version   GIF version

Theorem vprc 4724
 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
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nalset 4723 . . 3 ¬ ∃𝑥𝑦 𝑦𝑥
2 vex 3176 . . . . . . 7 𝑦 ∈ V
32tbt 358 . . . . . 6 (𝑦𝑥 ↔ (𝑦𝑥𝑦 ∈ V))
43albii 1737 . . . . 5 (∀𝑦 𝑦𝑥 ↔ ∀𝑦(𝑦𝑥𝑦 ∈ V))
5 dfcleq 2604 . . . . 5 (𝑥 = V ↔ ∀𝑦(𝑦𝑥𝑦 ∈ V))
64, 5bitr4i 266 . . . 4 (∀𝑦 𝑦𝑥𝑥 = V)
76exbii 1764 . . 3 (∃𝑥𝑦 𝑦𝑥 ↔ ∃𝑥 𝑥 = V)
81, 7mtbi 311 . 2 ¬ ∃𝑥 𝑥 = V
9 isset 3180 . 2 (V ∈ V ↔ ∃𝑥 𝑥 = V)
108, 9mtbir 312 1 ¬ V ∈ V
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 195  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977  Vcvv 3173 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709 This theorem depends on definitions:  df-bi 196  df-an 385  df-tru 1478  df-ex 1696  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175 This theorem is referenced by:  nvel  4725  vnex  4726  intex  4747  intnex  4748  snnex  6862  iprc  6993  elfi2  8203  fi0  8209  ruALT  8391  cardmin2  8707  00lsp  18802  bj-xnex  32245  fveqvfvv  39853  ndmaovcl  39932  opabn1stprc  40318
 Copyright terms: Public domain W3C validator