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

Theorem vprc 4590
 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

Proof of Theorem vprc
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nalset 4589 . . 3
2 vex 3112 . . . . . . 7
32tbt 344 . . . . . 6
43albii 1640 . . . . 5
5 dfcleq 2450 . . . . 5
64, 5bitr4i 252 . . . 4
76exbii 1667 . . 3
81, 7mtbi 298 . 2
9 isset 3113 . 2
108, 9mtbir 299 1
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  <->wb 184  A.wal 1393  =wceq 1395  E.wex 1612  e.wcel 1818   cvv 3109 This theorem is referenced by:  nvel  4591  vnex  4592  intex  4608  intnex  4609  snnex  6606  iprc  6735  elfi2  7894  fi0  7900  ruALT  8049  cardmin2  8400  00lsp  17627  fveqvfvv  32209  ndmaovcl  32288 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111
 Copyright terms: Public domain W3C validator