Theorem vprc 3449

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.

Assertion

Ref	Expression
vprc	|- -. _V e. _V

Proof of Theorem vprc

Step	Hyp	Ref	Expression
1		nalset 3448	. . 3 |- -. E.xA.y y e. x
2		visset 2295	. . . . . . 7 |- y e. _V
3	2	tbt 788	. . . . . 6 |- (y e. x <-> (y e. x <-> y e. _V))
4	3	albii 1346	. . . . 5 |- (A.y y e. x <-> A.y(y e. x <-> y e. _V))
5		dfcleq 1878	. . . . 5 |- (x = _V <-> A.y(y e. x <-> y e. _V))
6	4, 5	bitr4i 193	. . . 4 |- (A.y y e. x <-> x = _V)
7	6	exbii 1398	. . 3 |- (E.xA.y y e. x <-> E.x x = _V)
8	1, 7	mtbi 208	. 2 |- -. E.x x = _V
9		isset 2296	. 2 |- (_V e. _V <-> E.x x = _V)
10	8, 9	mtbir 209	1 |- -. _V e. _V

Syntax hints:  -. wn 2   <-> wb 163  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  _Vcvv 2292

This theorem is referenced by:  nvel 3450  vnex 3451  intex 3465  intnex 3466  snnex 3801  issetid 4121  issetidOLD 4122  iprc 4210  riotav 5565  ruALT 5705  fiuni 10219  fsubbas 10281  inpc 14619  elfiun 15369  inficl 15757

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-8 1306  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-ext 1865  ax-sep 3438

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294

Copyright terms: Public domain