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

Theorem vprc 4948
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 4947 . . 3 ¬ ∃𝑥𝑦 𝑦𝑥
2 vex 3343 . . . . . . 7 𝑦 ∈ V
32tbt 358 . . . . . 6 (𝑦𝑥 ↔ (𝑦𝑥𝑦 ∈ V))
43albii 1896 . . . . 5 (∀𝑦 𝑦𝑥 ↔ ∀𝑦(𝑦𝑥𝑦 ∈ V))
5 dfcleq 2754 . . . . 5 (𝑥 = V ↔ ∀𝑦(𝑦𝑥𝑦 ∈ V))
64, 5bitr4i 267 . . . 4 (∀𝑦 𝑦𝑥𝑥 = V)
76exbii 1923 . . 3 (∃𝑥𝑦 𝑦𝑥 ↔ ∃𝑥 𝑥 = V)
81, 7mtbi 311 . 2 ¬ ∃𝑥 𝑥 = V
9 isset 3347 . 2 (V ∈ V ↔ ∃𝑥 𝑥 = V)
108, 9mtbir 312 1 ¬ V ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wal 1630   = wceq 1632  wex 1853  wcel 2139  Vcvv 3340
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933
This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1635  df-ex 1854  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-v 3342
This theorem is referenced by:  nvel  4949  vnex  4950  intex  4969  intnex  4970  abnex  7131  snnexOLD  7133  iprc  7267  opabn1stprc  7396  elfi2  8487  fi0  8493  ruALT  8675  cardmin2  9034  00lsp  19203  fveqvfvv  41728  ndmaovcl  41807
  Copyright terms: Public domain W3C validator