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(x=y\wedge x=y\right)\to \left(x\in x\leftrightarrow y\in y\right)$$
2	1	anidms	$$⊢x=y\to \left(x\in x\leftrightarrow y\in y\right)$$
3	2	notbid	$$⊢x=y\to \left(\neg x\in x\leftrightarrow \neg y\in y\right)$$
4	3	cbvrabv	$$⊢\left\{x\in A|\neg x\in x\right\}=\left\{y\in A|\neg y\in y\right\}$$
5	4	eleq2i	$$⊢\left\{x\in A|\neg x\in x\right\}\in \left\{x\in A|\neg x\in x\right\}\leftrightarrow \left\{x\in A|\neg x\in x\right\}\in \left\{y\in A|\neg y\in y\right\}$$
6		elex	$$⊢\left\{x\in A|\neg x\in x\right\}\in \left\{y\in A|\neg y\in y\right\}\to \left\{x\in A|\neg x\in x\right\}\in \mathrm{V}$$
7		elex	$$⊢\left\{x\in A|\neg x\in x\right\}\in A\to \left\{x\in A|\neg x\in x\right\}\in \mathrm{V}$$
8	7	adantr	$$⊢\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)\to \left\{x\in A|\neg x\in x\right\}\in \mathrm{V}$$
9		eleq1	$$⊢y=z\to \left(y\in A\leftrightarrow z\in A\right)$$
10		id	$$⊢y=z\to y=z$$
11	10 10	eleq12d	$$⊢y=z\to \left(y\in y\leftrightarrow z\in z\right)$$
12	11	notbid	$$⊢y=z\to \left(\neg y\in y\leftrightarrow \neg z\in z\right)$$
13	9 12	anbi12d	$$⊢y=z\to \left(\left(y\in A\wedge \neg y\in y\right)\leftrightarrow \left(z\in A\wedge \neg z\in z\right)\right)$$
14		eleq1	$$⊢z=\left\{x\in A|\neg x\in x\right\}\to \left(z\in A\leftrightarrow \left\{x\in A|\neg x\in x\right\}\in A\right)$$
15		eleq12	$$⊢\left(z=\left\{x\in A|\neg x\in x\right\}\wedge z=\left\{x\in A|\neg x\in x\right\}\right)\to \left(z\in z\leftrightarrow \left\{x\in A|\neg x\in x\right\}\in \left\{x\in A|\neg x\in x\right\}\right)$$
16	15	anidms	$$⊢z=\left\{x\in A|\neg x\in x\right\}\to \left(z\in z\leftrightarrow \left\{x\in A|\neg x\in x\right\}\in \left\{x\in A|\neg x\in x\right\}\right)$$
17	16	notbid	$$⊢z=\left\{x\in A|\neg x\in x\right\}\to \left(\neg z\in z\leftrightarrow \neg \left\{x\in A|\neg x\in x\right\}\in \left\{x\in A|\neg x\in x\right\}\right)$$
18	14 17	anbi12d	$$⊢z=\left\{x\in A|\neg x\in x\right\}\to \left(\left(z\in A\wedge \neg z\in z\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)$$
19		df-rab	$$⊢\left\{y\in A|\neg y\in y\right\}=\left\{y|\left(y\in A\wedge \neg y\in y\right)\right\}$$
20	13 18 19	elab2gw	$$⊢\left\{x\in A|\neg x\in x\right\}\in \mathrm{V}\to \left(\left\{x\in A|\neg x\in x\right\}\in \left\{y\in A|\neg y\in y\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)$$
21	6 8 20	pm5.21nii	$$⊢\left\{x\in A|\neg x\in x\right\}\in \left\{y\in A|\neg y\in y\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)$$
22	5 21	bitri	$$⊢\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)$$
23		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$$
24	22 23	ax-mp	$$⊢\neg \left\{x\in A|\neg x\in x\right\}\in A$$