cnvsng

Description: Converse of a singleton of an ordered pair. (Contributed by NM, 23-Jan-2015) (Proof shortened by BJ, 12-Feb-2022)

		Ref	Expression
	Assertion	cnvsng	$⊢ (A \in V \land B \in W) \to {\{⟨A, B⟩\}}^{-1} = \{⟨B, A⟩\}$

Step	Hyp	Ref	Expression
1		cnvcnvsn	$⊢ {\{⟨B, A⟩\}}^{-1}^{-1} = {\{⟨A, B⟩\}}^{-1}$
2		relsnopg	$⊢ (B \in W \land A \in V) \to Rel \{⟨B, A⟩\}$
3	2	ancoms	$⊢ (A \in V \land B \in W) \to Rel \{⟨B, A⟩\}$
4		dfrel2	$⊢ Rel \{⟨B, A⟩\} \leftrightarrow {\{⟨B, A⟩\}}^{-1}^{-1} = \{⟨B, A⟩\}$
5	3 4	sylib	$⊢ (A \in V \land B \in W) \to {\{⟨B, A⟩\}}^{-1}^{-1} = \{⟨B, A⟩\}$
6	1 5	eqtr3id	$⊢ (A \in V \land B \in W) \to {\{⟨A, B⟩\}}^{-1} = \{⟨B, A⟩\}$

Metamath Proof Explorer