This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnvss

Description: Subset theorem for converse. (Contributed by NM, 22-Mar-1998) (Proof shortened by Kyle Wyonch, 27-Apr-2021)

		Ref	Expression
	Assertion	cnvss	$⊢ A \subseteq B \to A^{-1} \subseteq B^{-1}$

Step	Hyp	Ref	Expression
1		ssbr	$⊢ A \subseteq B \to (y A x \to y B x)$
2	1	ssopab2dv	$⊢ A \subseteq B \to \{⟨x, y⟩ \| y A x\} \subseteq \{⟨x, y⟩ \| y B x\}$
3		df-cnv	$⊢ A^{-1} = \{⟨x, y⟩ \| y A x\}$
4		df-cnv	$⊢ B^{-1} = \{⟨x, y⟩ \| y B x\}$
5	2 3 4	3sstr4g	$⊢ A \subseteq B \to A^{-1} \subseteq B^{-1}$