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

Metamath Proof Explorer

Theorem cnvsn

Description: Converse of a singleton of an ordered pair. (Contributed by NM, 11-May-1998) (Revised by Mario Carneiro, 26-Apr-2015) (Proof shortened by BJ, 12-Feb-2022)

	Ref	Expression
Hypotheses	cnvsn.1	$⊢ A \in V$
	cnvsn.2	$⊢ B \in V$
Assertion	cnvsn	$⊢ {\{⟨A, B⟩\}}^{-1} = \{⟨B, A⟩\}$

Proof

Step	Hyp	Ref	Expression
1		cnvsn.1	$⊢ A \in V$
2		cnvsn.2	$⊢ B \in V$
3		cnvsng	$⊢ (A \in V \land B \in V) \to {\{⟨A, B⟩\}}^{-1} = \{⟨B, A⟩\}$
4	1 2 3	mp2an	$⊢ {\{⟨A, B⟩\}}^{-1} = \{⟨B, A⟩\}$