Metamath Proof Explorer


Theorem 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 V B W A B -1 = B A

Proof

Step Hyp Ref Expression
1 cnvcnvsn B A -1 -1 = A B -1
2 relsnopg B W A V Rel B A
3 2 ancoms A V B W Rel B A
4 dfrel2 Rel B A B A -1 -1 = B A
5 3 4 sylib A V B W B A -1 -1 = B A
6 1 5 eqtr3id A V B W A B -1 = B A