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  7130  snnexOLD  7132  iprc  7266  opabn1stprc  7395  elfi2  8485  fi0  8491  ruALT  8673  cardmin2  9014  00lsp  19183  fveqvfvv  41710  ndmaovcl  41789
  Copyright terms: Public domain W3C validator