Metamath Proof Explorer

Theorem cnvsymOLD

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

Ref Expression
Assertion cnvsymOLD 
|- ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) )

Proof

Step Hyp Ref Expression
1 relcnv 
 |-  Rel `' R
2 ssrel3 
 |-  ( Rel `' R -> ( `' R C_ R <-> A. y A. x ( y `' R x -> y R x ) ) )
3 1 2 ax-mp 
 |-  ( `' R C_ R <-> A. y A. x ( y `' R x -> y R x ) )
4 alcom 
 |-  ( A. y A. x ( y `' R x -> y R x ) <-> A. x A. y ( y `' R x -> y R x ) )
5 vex 
 |-  y e. _V
6 vex 
 |-  x e. _V
7 5 6 brcnv 
 |-  ( y `' R x <-> x R y )
8 7 imbi1i 
 |-  ( ( y `' R x -> y R x ) <-> ( x R y -> y R x ) )
9 8 2albii 
 |-  ( A. x A. y ( y `' R x -> y R x ) <-> A. x A. y ( x R y -> y R x ) )
10 3 4 9 3bitri 
 |-  ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) )