Theorem ruOLD

Description: Obsolete version of ru as of 20-Jun-2025. (Contributed by NM, 7-Aug-1994) Remove use of ax-13 . (Revised by BJ, 12-Oct-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ruOLD	|- { x | x e/ x } e/ _V

Proof

Step	Hyp	Ref	Expression
1		pm5.19	|- -. ( y e. y <-> -. y e. y )
2		eleq1w	|- ( x = y -> ( x e. y <-> y e. y ) )
3		df-nel	|- ( x e/ x <-> -. x e. x )
4		id	|- ( x = y -> x = y )
5	4 4	eleq12d	|- ( x = y -> ( x e. x <-> y e. y ) )
6	5	notbid	|- ( x = y -> ( -. x e. x <-> -. y e. y ) )
7	3 6	bitrid	|- ( x = y -> ( x e/ x <-> -. y e. y ) )
8	2 7	bibi12d	|- ( x = y -> ( ( x e. y <-> x e/ x ) <-> ( y e. y <-> -. y e. y ) ) )
9	8	spvv	|- ( A. x ( x e. y <-> x e/ x ) -> ( y e. y <-> -. y e. y ) )
10	1 9	mto	|- -. A. x ( x e. y <-> x e/ x )
11		eqabb	|- ( y = { x | x e/ x } <-> A. x ( x e. y <-> x e/ x ) )
12	10 11	mtbir	|- -. y = { x | x e/ x }
13	12	nex	|- -. E. y y = { x | x e/ x }
14		isset	|- ( { x | x e/ x } e. _V <-> E. y y = { x | x e/ x } )
15	13 14	mtbir	|- -. { x | x e/ x } e. _V
16	15	nelir	|- { x | x e/ x } e/ _V