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\left(\left(x\left({R\upharpoonright }_{\left\{A\right\}}\right)y\wedge y\left({R\upharpoonright }_{\left\{A\right\}}\right)x\right)\to x=y\right)$$

Proof

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