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 ) )