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.

Step	Hyp	Ref	Expression
1		nalset 4589	. . 3
2		vex 3112	. . . . . . 7
3	2	tbt 344	. . . . . 6
4	3	albii 1640	. . . . 5
5		dfcleq 2450	. . . . 5
6	4, 5	bitr4i 252	. . . 4
7	6	exbii 1667	. . 3
8	1, 7	mtbi 298	. 2
9		isset 3113	. 2
10	8, 9	mtbir 299	1

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