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

Theorem vprc 4233
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  e.  _V

Proof of Theorem vprc
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nalset 4232 . . 3  |-  -.  E. x A. y  y  e.  x
2 vex 2867 . . . . . . 7  |-  y  e. 
_V
32tbt 333 . . . . . 6  |-  ( y  e.  x  <->  ( y  e.  x  <->  y  e.  _V ) )
43albii 1566 . . . . 5  |-  ( A. y  y  e.  x  <->  A. y ( y  e.  x  <->  y  e.  _V ) )
5 dfcleq 2352 . . . . 5  |-  ( x  =  _V  <->  A. y
( y  e.  x  <->  y  e.  _V ) )
64, 5bitr4i 243 . . . 4  |-  ( A. y  y  e.  x  <->  x  =  _V )
76exbii 1582 . . 3  |-  ( E. x A. y  y  e.  x  <->  E. x  x  =  _V )
81, 7mtbi 289 . 2  |-  -.  E. x  x  =  _V
9 isset 2868 . 2  |-  ( _V  e.  _V  <->  E. x  x  =  _V )
108, 9mtbir 290 1  |-  -.  _V  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176   A.wal 1540   E.wex 1541    = wceq 1642    e. wcel 1710   _Vcvv 2864
This theorem is referenced by:  nvel  4234  vnex  4235  intex  4248  intnex  4249  snnex  4606  iprc  5025  riotav  6396  elfi2  7258  fi0  7263  ruALT  7405  cardmin2  7721  00lsp  15837  fveqvfvv  27312  ndmaovcl  27391
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-v 2866
  Copyright terms: Public domain W3C validator