Theorem ssrel3

Description: Subclass relation in another form when the subclass is a relation. (Contributed by Peter Mazsa, 16-Feb-2019)

	Ref	Expression
Assertion	ssrel3	$$⊢\mathrm{Rel}A\to \left(A\subseteq B\leftrightarrow \forall x\forall y\left(xAy\to xBy\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssrel	$$⊢\mathrm{Rel}A\to \left(A\subseteq B\leftrightarrow \forall x\forall y\left(⟨x,y⟩\in A\to ⟨x,y⟩\in B\right)\right)$$
2		df-br	$$⊢xAy\leftrightarrow ⟨x,y⟩\in A$$
3		df-br	$$⊢xBy\leftrightarrow ⟨x,y⟩\in B$$
4	2 3	imbi12i	$$⊢\left(xAy\to xBy\right)\leftrightarrow \left(⟨x,y⟩\in A\to ⟨x,y⟩\in B\right)$$
5	4	2albii	$$⊢\forall x\forall y\left(xAy\to xBy\right)\leftrightarrow \forall x\forall y\left(⟨x,y⟩\in A\to ⟨x,y⟩\in B\right)$$
6	1 5	bitr4di	$$⊢\mathrm{Rel}A\to \left(A\subseteq B\leftrightarrow \forall x\forall y\left(xAy\to xBy\right)\right)$$