This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )