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	⊢ ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴

Proof

Step	Hyp	Ref	Expression
1		eleq12	⊢ ( ( 𝑦 = { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∧ 𝑦 = { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) → ( 𝑦 ∈ 𝑦 ↔ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) )
2	1	anidms	⊢ ( 𝑦 = { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } → ( 𝑦 ∈ 𝑦 ↔ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) )
3	2	notbid	⊢ ( 𝑦 = { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } → ( ¬ 𝑦 ∈ 𝑦 ↔ ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) )
4		eleq12	⊢ ( ( 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦 ) )
5	4	anidms	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦 ) )
6	5	notbid	⊢ ( 𝑥 = 𝑦 → ( ¬ 𝑥 ∈ 𝑥 ↔ ¬ 𝑦 ∈ 𝑦 ) )
7	6	cbvrabv	⊢ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } = { 𝑦 ∈ 𝐴 ∣ ¬ 𝑦 ∈ 𝑦 }
8	3 7	elrab2	⊢ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ↔ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴 ∧ ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) )
9		pclem6	⊢ ( ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ↔ ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴 ∧ ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ) ) → ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴 )
10	8 9	ax-mp	⊢ ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴