Theorem antisymressn

Description: Every class ' R ' restricted to the singleton of the class ' A ' (see ressn2 ) is antisymmetric. (Contributed by Peter Mazsa, 11-Jun-2024)

	Ref	Expression
Assertion	antisymressn	⊢ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑦 ∧ 𝑦 ( 𝑅 ↾ { 𝐴 } ) 𝑥 ) → 𝑥 = 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		brressn	⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑦 ↔ ( 𝑥 = 𝐴 ∧ 𝑥 𝑅 𝑦 ) ) )
2	1	el2v	⊢ ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑦 ↔ ( 𝑥 = 𝐴 ∧ 𝑥 𝑅 𝑦 ) )
3	2	simplbi	⊢ ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑦 → 𝑥 = 𝐴 )
4		brressn	⊢ ( ( 𝑦 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑦 ( 𝑅 ↾ { 𝐴 } ) 𝑥 ↔ ( 𝑦 = 𝐴 ∧ 𝑦 𝑅 𝑥 ) ) )
5	4	el2v	⊢ ( 𝑦 ( 𝑅 ↾ { 𝐴 } ) 𝑥 ↔ ( 𝑦 = 𝐴 ∧ 𝑦 𝑅 𝑥 ) )
6	5	simplbi	⊢ ( 𝑦 ( 𝑅 ↾ { 𝐴 } ) 𝑥 → 𝑦 = 𝐴 )
7		eqtr3	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐴 ) → 𝑥 = 𝑦 )
8	3 6 7	syl2an	⊢ ( ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑦 ∧ 𝑦 ( 𝑅 ↾ { 𝐴 } ) 𝑥 ) → 𝑥 = 𝑦 )
9	8	gen2	⊢ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ( 𝑅 ↾ { 𝐴 } ) 𝑦 ∧ 𝑦 ( 𝑅 ↾ { 𝐴 } ) 𝑥 ) → 𝑥 = 𝑦 )