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	$$⊢\neg \left\{x\in A|\neg x\in x\right\}\in A$$

Proof

Step	Hyp	Ref	Expression
1		eleq12	$$⊢\left(y=\left\{x\in A|\neg x\in x\right\}\wedge y=\left\{x\in A|\neg x\in x\right\}\right)\to \left(y\in y\leftrightarrow \left\{x\in A|\neg x\in x\right\}\in \left\{x\in A|\neg x\in x\right\}\right)$$
2	1	anidms	$$⊢y=\left\{x\in A|\neg x\in x\right\}\to \left(y\in y\leftrightarrow \left\{x\in A|\neg x\in x\right\}\in \left\{x\in A|\neg x\in x\right\}\right)$$
3	2	notbid	$$⊢y=\left\{x\in A|\neg x\in x\right\}\to \left(\neg y\in y\leftrightarrow \neg \left\{x\in A|\neg x\in x\right\}\in \left\{x\in A|\neg x\in x\right\}\right)$$
4		eleq12	$$⊢\left(x=y\wedge x=y\right)\to \left(x\in x\leftrightarrow y\in y\right)$$
5	4	anidms	$$⊢x=y\to \left(x\in x\leftrightarrow y\in y\right)$$
6	5	notbid	$$⊢x=y\to \left(\neg x\in x\leftrightarrow \neg y\in y\right)$$
7	6	cbvrabv	$$⊢\left\{x\in A|\neg x\in x\right\}=\left\{y\in A|\neg y\in y\right\}$$
8	3 7	elrab2	$$⊢\left\{x\in A|\neg x\in x\right\}\in \left\{x\in A|\neg x\in x\right\}\leftrightarrow \left(\left\{x\in A|\neg x\in x\right\}\in A\wedge \neg \left\{x\in A|\neg x\in x\right\}\in \left\{x\in A|\neg x\in x\right\}\right)$$
9		pclem6	$$⊢\left(\left\{x\in A|\neg x\in x\right\}\in \left\{x\in A|\neg x\in x\right\}\leftrightarrow \left(\left\{x\in A|\neg x\in x\right\}\in A\wedge \neg \left\{x\in A|\neg x\in x\right\}\in \left\{x\in A|\neg x\in x\right\}\right)\right)\to \neg \left\{x\in A|\neg x\in x\right\}\in A$$
10	8 9	ax-mp	$$⊢\neg \left\{x\in A|\neg x\in x\right\}\in A$$