Theorem rru

Description: Relative version of Russell's paradox ru (which corresponds to the case A = _V ).

Originally a subproof in pwnss . (Contributed by Stefan O'Rear, 22-Feb-2015) Avoid df-nel . (Revised by Steven Nguyen, 23-Nov-2022) Reduce axiom usage. (Revised by Gino Giotto, 30-Aug-2024)

	Ref	Expression
Assertion	rru	|- -. { x e. A | -. x e. x } e. A

Proof

Step	Hyp	Ref	Expression
1		eleq12	|- ( ( x = y /\ x = y ) -> ( x e. x <-> y e. y ) )
2	1	anidms	|- ( x = y -> ( x e. x <-> y e. y ) )
3	2	notbid	|- ( x = y -> ( -. x e. x <-> -. y e. y ) )
4	3	cbvrabv	|- { x e. A | -. x e. x } = { y e. A | -. y e. y }
5	4	eleq2i	|- ( { x e. A | -. x e. x } e. { x e. A | -. x e. x } <-> { x e. A | -. x e. x } e. { y e. A | -. y e. y } )
6		elex	|- ( { x e. A | -. x e. x } e. { y e. A | -. y e. y } -> { x e. A | -. x e. x } e. _V )
7		elex	|- ( { x e. A | -. x e. x } e. A -> { x e. A | -. x e. x } e. _V )
8	7	adantr	|- ( ( { 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. _V )
9		eleq1	|- ( y = z -> ( y e. A <-> z e. A ) )
10		id	|- ( y = z -> y = z )
11	10 10	eleq12d	|- ( y = z -> ( y e. y <-> z e. z ) )
12	11	notbid	|- ( y = z -> ( -. y e. y <-> -. z e. z ) )
13	9 12	anbi12d	|- ( y = z -> ( ( y e. A /\ -. y e. y ) <-> ( z e. A /\ -. z e. z ) ) )
14		eleq1	|- ( z = { x e. A | -. x e. x } -> ( z e. A <-> { x e. A | -. x e. x } e. A ) )
15		eleq12	|- ( ( z = { x e. A | -. x e. x } /\ z = { x e. A | -. x e. x } ) -> ( z e. z <-> { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) )
16	15	anidms	|- ( z = { x e. A | -. x e. x } -> ( z e. z <-> { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) )
17	16	notbid	|- ( z = { x e. A | -. x e. x } -> ( -. z e. z <-> -. { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) )
18	14 17	anbi12d	|- ( z = { x e. A | -. x e. x } -> ( ( z e. A /\ -. z e. z ) <-> ( { x e. A | -. x e. x } e. A /\ -. { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) ) )
19		df-rab	|- { y e. A | -. y e. y } = { y | ( y e. A /\ -. y e. y ) }
20	13 18 19	elab2gw	|- ( { x e. A | -. x e. x } e. _V -> ( { x e. A | -. x e. x } e. { y e. A | -. y e. y } <-> ( { x e. A | -. x e. x } e. A /\ -. { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) ) )
21	6 8 20	pm5.21nii	|- ( { x e. A | -. x e. x } e. { y e. A | -. y e. y } <-> ( { x e. A | -. x e. x } e. A /\ -. { x e. A | -. x e. x } e. { x e. A | -. x e. x } ) )
22	5 21	bitri	|- ( { 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 } ) )
23		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 )
24	22 23	ax-mp	|- -. { x e. A | -. x e. x } e. A