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

Theorem vprc 4301
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 4300 . . 3  |-  -.  E. x A. y  y  e.  x
2 vex 2919 . . . . . . 7  |-  y  e. 
_V
32tbt 334 . . . . . 6  |-  ( y  e.  x  <->  ( y  e.  x  <->  y  e.  _V ) )
43albii 1572 . . . . 5  |-  ( A. y  y  e.  x  <->  A. y ( y  e.  x  <->  y  e.  _V ) )
5 dfcleq 2398 . . . . 5  |-  ( x  =  _V  <->  A. y
( y  e.  x  <->  y  e.  _V ) )
64, 5bitr4i 244 . . . 4  |-  ( A. y  y  e.  x  <->  x  =  _V )
76exbii 1589 . . 3  |-  ( E. x A. y  y  e.  x  <->  E. x  x  =  _V )
81, 7mtbi 290 . 2  |-  -.  E. x  x  =  _V
9 isset 2920 . 2  |-  ( _V  e.  _V  <->  E. x  x  =  _V )
108, 9mtbir 291 1  |-  -.  _V  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177   A.wal 1546   E.wex 1547    = wceq 1649    e. wcel 1721   _Vcvv 2916
This theorem is referenced by:  nvel  4302  vnex  4303  intex  4316  intnex  4317  snnex  4672  iprc  5093  riotav  6513  elfi2  7377  fi0  7383  ruALT  7525  cardmin2  7841  00lsp  16012  fveqvfvv  27855  ndmaovcl  27934
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-v 2918
  Copyright terms: Public domain W3C validator