Metamath Proof Explorer

Theorem cnvsym

Description: Two ways of saying a relation is symmetric. Similar to definition of symmetry in Schechter p. 51. (Contributed by NM, 28-Dec-1996) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof shortened by SN, 23-Dec-2024) Avoid ax-11 . (Revised by BTernaryTau, 29-Dec-2024)

Ref Expression
Assertion cnvsym 
|- ( `' 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 breq1 
 |-  ( y = z -> ( y `' R x <-> z `' R x ) )
5 breq1 
 |-  ( y = z -> ( y R x <-> z R x ) )
6 4 5 imbi12d 
 |-  ( y = z -> ( ( y `' R x -> y R x ) <-> ( z `' R x -> z R x ) ) )
7 breq2 
 |-  ( x = z -> ( y `' R x <-> y `' R z ) )
8 breq2 
 |-  ( x = z -> ( y R x <-> y R z ) )
9 7 8 imbi12d 
 |-  ( x = z -> ( ( y `' R x -> y R x ) <-> ( y `' R z -> y R z ) ) )
10 6 9 alcomw 
 |-  ( A. y A. x ( y `' R x -> y R x ) <-> A. x A. y ( y `' R x -> y R x ) )
11 vex 
 |-  y e. _V
12 vex 
 |-  x e. _V
13 11 12 brcnv 
 |-  ( y `' R x <-> x R y )
14 13 imbi1i 
 |-  ( ( y `' R x -> y R x ) <-> ( x R y -> y R x ) )
15 14 2albii 
 |-  ( A. x A. y ( y `' R x -> y R x ) <-> A. x A. y ( x R y -> y R x ) )
16 3 10 15 3bitri 
 |-  ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) )