Theorem brssr

Description: The subset relation and subclass relationship ( df-ss ) are the same, that is, ( AS B <-> A C B ) when B is a set. (Contributed by Peter Mazsa, 31-Jul-2019)

	Ref	Expression
Assertion	brssr	$$⊢B\in V\to \left(A\mathrm{S}B\leftrightarrow A\subseteq B\right)$$

Proof

Step	Hyp	Ref	Expression
1		relssr	$$⊢\mathrm{Rel}\mathrm{S}$$
2	1	brrelex1i	$$⊢A\mathrm{S}B\to A\in \mathrm{V}$$
3	2	adantl	$$⊢\left(B\in V\wedge A\mathrm{S}B\right)\to A\in \mathrm{V}$$
4		simpl	$$⊢\left(B\in V\wedge A\mathrm{S}B\right)\to B\in V$$
5	3 4	jca	$$⊢\left(B\in V\wedge A\mathrm{S}B\right)\to \left(A\in \mathrm{V}\wedge B\in V\right)$$
6		ssexg	$$⊢\left(A\subseteq B\wedge B\in V\right)\to A\in \mathrm{V}$$
7		simpr	$$⊢\left(A\subseteq B\wedge B\in V\right)\to B\in V$$
8	6 7	jca	$$⊢\left(A\subseteq B\wedge B\in V\right)\to \left(A\in \mathrm{V}\wedge B\in V\right)$$
9	8	ancoms	$$⊢\left(B\in V\wedge A\subseteq B\right)\to \left(A\in \mathrm{V}\wedge B\in V\right)$$
10		sseq1	$$⊢x=A\to \left(x\subseteq y\leftrightarrow A\subseteq y\right)$$
11		sseq2	$$⊢y=B\to \left(A\subseteq y\leftrightarrow A\subseteq B\right)$$
12		df-ssr	$$⊢\mathrm{S}=\left\{⟨x,y⟩|x\subseteq y\right\}$$
13	10 11 12	brabg	$$⊢\left(A\in \mathrm{V}\wedge B\in V\right)\to \left(A\mathrm{S}B\leftrightarrow A\subseteq B\right)$$
14	5 9 13	pm5.21nd	$$⊢B\in V\to \left(A\mathrm{S}B\leftrightarrow A\subseteq B\right)$$