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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alcom | |
|
2 | relcnv | |
|
3 | ssrel | |
|
4 | 2 3 | ax-mp | |
5 | vex | |
|
6 | vex | |
|
7 | 5 6 | brcnv | |
8 | df-br | |
|
9 | 7 8 | bitr3i | |
10 | df-br | |
|
11 | 9 10 | imbi12i | |
12 | 11 | 2albii | |
13 | 1 4 12 | 3bitr4i | |