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	$⊢ \forall x \forall y ((x ({R ↾}_{\{A\}}) y \land y ({R ↾}_{\{A\}}) x) \to x = y)$

Proof

Step	Hyp	Ref	Expression
1		brressn	$⊢ (x \in V \land y \in V) \to (x ({R ↾}_{\{A\}}) y \leftrightarrow (x = A \land x R y))$
2	1	el2v	$⊢ x ({R ↾}_{\{A\}}) y \leftrightarrow (x = A \land x R y)$
3	2	simplbi	$⊢ x ({R ↾}_{\{A\}}) y \to x = A$
4		brressn	$⊢ (y \in V \land x \in V) \to (y ({R ↾}_{\{A\}}) x \leftrightarrow (y = A \land y R x))$
5	4	el2v	$⊢ y ({R ↾}_{\{A\}}) x \leftrightarrow (y = A \land y R x)$
6	5	simplbi	$⊢ y ({R ↾}_{\{A\}}) x \to y = A$
7		eqtr3	$⊢ (x = A \land y = A) \to x = y$
8	3 6 7	syl2an	$⊢ (x ({R ↾}_{\{A\}}) y \land y ({R ↾}_{\{A\}}) x) \to x = y$
9	8	gen2	$⊢ \forall x \forall y ((x ({R ↾}_{\{A\}}) y \land y ({R ↾}_{\{A\}}) x) \to x = y)$