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

Theorem vprc 4154
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 4153 . . 3  |-  -.  E. x A. y  y  e.  x
2 vex 2793 . . . . . . 7  |-  y  e. 
_V
32tbt 333 . . . . . 6  |-  ( y  e.  x  <->  ( y  e.  x  <->  y  e.  _V ) )
43albii 1555 . . . . 5  |-  ( A. y  y  e.  x  <->  A. y ( y  e.  x  <->  y  e.  _V ) )
5 dfcleq 2279 . . . . 5  |-  ( x  =  _V  <->  A. y
( y  e.  x  <->  y  e.  _V ) )
64, 5bitr4i 243 . . . 4  |-  ( A. y  y  e.  x  <->  x  =  _V )
76exbii 1571 . . 3  |-  ( E. x A. y  y  e.  x  <->  E. x  x  =  _V )
81, 7mtbi 289 . 2  |-  -.  E. x  x  =  _V
9 isset 2794 . 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 1529   E.wex 1530    = wceq 1625    e. wcel 1686   _Vcvv 2790
This theorem is referenced by:  nvel  4155  vnex  4156  intex  4169  intnex  4170  snnex  4526  iprc  4945  riotav  6311  elfi2  7170  fi0  7175  ruALT  7317  cardmin2  7633  00lsp  15740  inpc  25288  fveqvfvv  27998  ndmaovcl  28074
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-v 2792
  Copyright terms: Public domain W3C validator