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 \mathrm{V}$$
	cnvsn.2	$$⊢B\in \mathrm{V}$$
Assertion	cnvsn	$$⊢{\left\{⟨A,B⟩\right\}}^{-1}=\left\{⟨B,A⟩\right\}$$

Proof

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