Metamath Proof Explorer

Theorem rruOLD

Description: Obsolete version of rru as of 30-Aug-2024. (Contributed by Stefan O'Rear, 22-Feb-2015) Avoid df-nel . (Revised by Steven Nguyen, 23-Nov-2022) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	rruOLD	\|- -. { x e. A \| -. x e. x } e. A

Proof

Step	Hyp	Ref	Expression
1		eleq12	\|- ( ( y = { x e. A \| -. x e. x } /\ y = { x e. A \| -. x e. x } ) -> ( y e. y <-> { x e. A \| -. x e. x } e. { x e. A \| -. x e. x } ) )
2	1	anidms	\|- ( y = { x e. A \| -. x e. x } -> ( y e. y <-> { x e. A \| -. x e. x } e. { x e. A \| -. x e. x } ) )
3	2	notbid	\|- ( y = { x e. A \| -. x e. x } -> ( -. y e. y <-> -. { x e. A \| -. x e. x } e. { x e. A \| -. x e. x } ) )
4		eleq12	\|- ( ( x = y /\ x = y ) -> ( x e. x <-> y e. y ) )
5	4	anidms	\|- ( x = y -> ( x e. x <-> y e. y ) )
6	5	notbid	\|- ( x = y -> ( -. x e. x <-> -. y e. y ) )
7	6	cbvrabv	\|- { x e. A \| -. x e. x } = { y e. A \| -. y e. y }
8	3 7	elrab2	\|- ( { x e. A \| -. x e. x } e. { x e. A \| -. x e. x } <-> ( { x e. A \| -. x e. x } e. A /\ -. { x e. A \| -. x e. x } e. { x e. A \| -. x e. x } ) )
9		pclem6	\|- ( ( { x e. A \| -. x e. x } e. { x e. A \| -. x e. x } <-> ( { x e. A \| -. x e. x } e. A /\ -. { x e. A \| -. x e. x } e. { x e. A \| -. x e. x } ) ) -> -. { x e. A \| -. x e. x } e. A )
10	8 9	ax-mp	\|- -. { x e. A \| -. x e. x } e. A