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 e. V /\ B e. W ) -> `' { <. A , B >. } = { <. B , A >. } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnvcnvsn | |- `' `' { <. B , A >. } = `' { <. A , B >. } |
|
2 | relsnopg | |- ( ( B e. W /\ A e. V ) -> Rel { <. B , A >. } ) |
|
3 | 2 | ancoms | |- ( ( A e. V /\ B e. W ) -> Rel { <. B , A >. } ) |
4 | dfrel2 | |- ( Rel { <. B , A >. } <-> `' `' { <. B , A >. } = { <. B , A >. } ) |
|
5 | 3 4 | sylib | |- ( ( A e. V /\ B e. W ) -> `' `' { <. B , A >. } = { <. B , A >. } ) |
6 | 1 5 | eqtr3id | |- ( ( A e. V /\ B e. W ) -> `' { <. A , B >. } = { <. B , A >. } ) |