cnveq

Description: Equality theorem for converse relation. (Contributed by NM, 13-Aug-1995)

		Ref	Expression
	Assertion	cnveq	$⊢ A = B \to A^{-1} = B^{-1}$

Step	Hyp	Ref	Expression
1		cnvss	$⊢ A \subseteq B \to A^{-1} \subseteq B^{-1}$
2		cnvss	$⊢ B \subseteq A \to B^{-1} \subseteq A^{-1}$
3	1 2	anim12i	$⊢ (A \subseteq B \land B \subseteq A) \to (A^{-1} \subseteq B^{-1} \land B^{-1} \subseteq A^{-1})$
4		eqss	$⊢ A = B \leftrightarrow (A \subseteq B \land B \subseteq A)$
5		eqss	$⊢ A^{-1} = B^{-1} \leftrightarrow (A^{-1} \subseteq B^{-1} \land B^{-1} \subseteq A^{-1})$
6	3 4 5	3imtr4i	$⊢ A = B \to A^{-1} = B^{-1}$

Metamath Proof Explorer