Theorem ruALT 4617

Description: Alternate proof of Russell's Paradox ru 1945, simplified using (indirectly) the Axiom of Regularity ax-reg 4608. (Contributed by Alan Sare, 4-Oct-2008.)

Assertion

Ref	Expression
ruALT	|- {x | x e/ x} e/ V

Proof of Theorem ruALT

Step	Hyp	Ref	Expression
1		nvelv 2728	. . 3 |- -. V e. V
2		df-nel 1595	. . 3 |- (V e/ V <-> -. V e. V)
3	1, 2	mpbir 190	. 2 |- V e/ V
4		ruv 4616	. . 3 |- {x | x e/ x} = V
5		neleq1 1649	. . 3 |- ({x | x e/ x} = V -> ({x | x e/ x} e/ V <-> V e/ V))
6	4, 5	ax-mp 7	. 2 |- ({x | x e/ x} e/ V <-> V e/ V)
7	3, 6	mpbir 190	1 |- {x | x e/ x} e/ V

Syntax hints:  -. wn 2   <-> wb 146   = wceq 960   e. wcel 962  {cab 1469   e/ wnel 1593  Vcvv 1818

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-10o 1144  ax-16 1214  ax-11o 1222  ax-ext 1464  ax-sep 2718  ax-pow 2758  ax-reg 4608

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 985  df-sb 1176  df-eu 1386  df-mo 1387  df-clab 1470  df-cleq 1475  df-clel 1478  df-ne 1594  df-nel 1595  df-ral 1656  df-rex 1657  df-v 1819  df-dif 2060  df-un 2061  df-in 2062  df-ss 2064  df-nul 2292  df-pw 2414  df-sn 2424  df-pr 2425

Copyright terms: Public domain