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)

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

Proof

Step Hyp Ref Expression
1 alcom
 |-  ( A. y A. x ( <. y , x >. e. `' R -> <. y , x >. e. R ) <-> A. x A. y ( <. y , x >. e. `' R -> <. y , x >. e. R ) )
2 relcnv
 |-  Rel `' R
3 ssrel
 |-  ( Rel `' R -> ( `' R C_ R <-> A. y A. x ( <. y , x >. e. `' R -> <. y , x >. e. R ) ) )
4 2 3 ax-mp
 |-  ( `' R C_ R <-> A. y A. x ( <. y , x >. e. `' R -> <. y , x >. e. R ) )
5 vex
 |-  y e. _V
6 vex
 |-  x e. _V
7 5 6 brcnv
 |-  ( y `' R x <-> x R y )
8 df-br
 |-  ( y `' R x <-> <. y , x >. e. `' R )
9 7 8 bitr3i
 |-  ( x R y <-> <. y , x >. e. `' R )
10 df-br
 |-  ( y R x <-> <. y , x >. e. R )
11 9 10 imbi12i
 |-  ( ( x R y -> y R x ) <-> ( <. y , x >. e. `' R -> <. y , x >. e. R ) )
12 11 2albii
 |-  ( A. x A. y ( x R y -> y R x ) <-> A. x A. y ( <. y , x >. e. `' R -> <. y , x >. e. R ) )
13 1 4 12 3bitr4i
 |-  ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) )