Metamath Proof Explorer


Theorem cnvsymOLDOLD

Description: Obsolete proof of cnvsym as of 23-Dec-2024. (Contributed by NM, 28-Dec-1996) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cnvsymOLDOLD R-1RxyxRyyRx

Proof

Step Hyp Ref Expression
1 alcom yxyxR-1yxRxyyxR-1yxR
2 relcnv RelR-1
3 ssrel RelR-1R-1RyxyxR-1yxR
4 2 3 ax-mp R-1RyxyxR-1yxR
5 vex yV
6 vex xV
7 5 6 brcnv yR-1xxRy
8 df-br yR-1xyxR-1
9 7 8 bitr3i xRyyxR-1
10 df-br yRxyxR
11 9 10 imbi12i xRyyRxyxR-1yxR
12 11 2albii xyxRyyRxxyyxR-1yxR
13 1 4 12 3bitr4i R-1RxyxRyyRx