Theorem extssr

Description: Property of subset relation, see also extid , extep and the comment of df-ssr . (Contributed by Peter Mazsa, 10-Jul-2019)

	Ref	Expression
Assertion	extssr	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\left[A\right]{\mathrm{S}}^{-1}=\left[B\right]{\mathrm{S}}^{-1}\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		brssr	$$⊢A\in V\to \left(x\mathrm{S}A\leftrightarrow x\subseteq A\right)$$
2		brssr	$$⊢B\in W\to \left(x\mathrm{S}B\leftrightarrow x\subseteq B\right)$$
3	1 2	bi2bian9	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\left(x\mathrm{S}A\leftrightarrow x\mathrm{S}B\right)\leftrightarrow \left(x\subseteq A\leftrightarrow x\subseteq B\right)\right)$$
4	3	albidv	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\forall x\left(x\mathrm{S}A\leftrightarrow x\mathrm{S}B\right)\leftrightarrow \forall x\left(x\subseteq A\leftrightarrow x\subseteq B\right)\right)$$
5		relssr	$$⊢\mathrm{Rel}\mathrm{S}$$
6		releccnveq	$$⊢\left(\mathrm{Rel}\mathrm{S}\wedge \mathrm{Rel}\mathrm{S}\right)\to \left(\left[A\right]{\mathrm{S}}^{-1}=\left[B\right]{\mathrm{S}}^{-1}\leftrightarrow \forall x\left(x\mathrm{S}A\leftrightarrow x\mathrm{S}B\right)\right)$$
7	5 5 6	mp2an	$$⊢\left[A\right]{\mathrm{S}}^{-1}=\left[B\right]{\mathrm{S}}^{-1}\leftrightarrow \forall x\left(x\mathrm{S}A\leftrightarrow x\mathrm{S}B\right)$$
8		ssext	$$⊢A=B\leftrightarrow \forall x\left(x\subseteq A\leftrightarrow x\subseteq B\right)$$
9	4 7 8	3bitr4g	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\left[A\right]{\mathrm{S}}^{-1}=\left[B\right]{\mathrm{S}}^{-1}\leftrightarrow A=B\right)$$