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 e. _V
	cnvsn.2	|- B e. _V
Assertion	cnvsn	|- `' { <. A , B >. } = { <. B , A >. }

Proof

Step	Hyp	Ref	Expression
1		cnvsn.1	|- A e. _V
2		cnvsn.2	|- B e. _V
3		cnvsng	|- ( ( A e. _V /\ B e. _V ) -> `' { <. A , B >. } = { <. B , A >. } )
4	1 2 3	mp2an	|- `' { <. A , B >. } = { <. B , A >. }