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

Theorem vprc 4153
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 4152 . . 3  |-  -.  E. x A. y  y  e.  x
2 vex 2792 . . . . . . 7  |-  y  e. 
_V
32tbt 333 . . . . . 6  |-  ( y  e.  x  <->  ( y  e.  x  <->  y  e.  _V ) )
43albii 1553 . . . . 5  |-  ( A. y  y  e.  x  <->  A. y ( y  e.  x  <->  y  e.  _V ) )
5 dfcleq 2278 . . . . 5  |-  ( x  =  _V  <->  A. y
( y  e.  x  <->  y  e.  _V ) )
64, 5bitr4i 243 . . . 4  |-  ( A. y  y  e.  x  <->  x  =  _V )
76exbii 1569 . . 3  |-  ( E. x A. y  y  e.  x  <->  E. x  x  =  _V )
81, 7mtbi 289 . 2  |-  -.  E. x  x  =  _V
9 isset 2793 . 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 1527   E.wex 1528    = wceq 1623    e. wcel 1685   _Vcvv 2789
This theorem is referenced by:  nvel  4154  vnex  4155  intex  4170  intnex  4171  snnex  4523  iprc  4942  riotav  6305  elfi2  7164  fi0  7169  ruALT  7311  cardmin2  7627  00lsp  15734  inpc  24688  fveqvfvv  27378  ndmaovcl  27454
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-v 2791
  Copyright terms: Public domain W3C validator