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	|- A. x A. y ( ( x ( R |` { A } ) y /\ y ( R |` { A } ) x ) -> x = y )

Proof

Step	Hyp	Ref	Expression
1		brressn	|- ( ( x e. _V /\ y e. _V ) -> ( x ( R |` { A } ) y <-> ( x = A /\ x R y ) ) )
2	1	el2v	|- ( x ( R |` { A } ) y <-> ( x = A /\ x R y ) )
3	2	simplbi	|- ( x ( R |` { A } ) y -> x = A )
4		brressn	|- ( ( y e. _V /\ x e. _V ) -> ( y ( R |` { A } ) x <-> ( y = A /\ y R x ) ) )
5	4	el2v	|- ( y ( R |` { A } ) x <-> ( y = A /\ y R x ) )
6	5	simplbi	|- ( y ( R |` { A } ) x -> y = A )
7		eqtr3	|- ( ( x = A /\ y = A ) -> x = y )
8	3 6 7	syl2an	|- ( ( x ( R |` { A } ) y /\ y ( R |` { A } ) x ) -> x = y )
9	8	gen2	|- A. x A. y ( ( x ( R |` { A } ) y /\ y ( R |` { A } ) x ) -> x = y )