ssrel3

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

		Ref	Expression
	Assertion	ssrel3	$⊢ Rel A \to (A \subseteq B \leftrightarrow \forall x \forall y (x A y \to x B y))$

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

Metamath Proof Explorer