Theorem relcnveq2

Description: Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 28-Apr-2019)

	Ref	Expression
Assertion	relcnveq2	|- ( Rel R -> ( `' R = R <-> A. x A. y ( x R y <-> y R x ) ) )

Proof

Step	Hyp	Ref	Expression
1		cnvsym	|- ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) )
2	1	a1i	|- ( Rel R -> ( `' R C_ R <-> A. x A. y ( x R y -> y R x ) ) )
3		dfrel2	|- ( Rel R <-> `' `' R = R )
4	3	biimpi	|- ( Rel R -> `' `' R = R )
5	4	sseq1d	|- ( Rel R -> ( `' `' R C_ `' R <-> R C_ `' R ) )
6		cnvsym	|- ( `' `' R C_ `' R <-> A. x A. y ( x `' R y -> y `' R x ) )
7	5 6	bitr3di	|- ( Rel R -> ( R C_ `' R <-> A. x A. y ( x `' R y -> y `' R x ) ) )
8		relbrcnvg	|- ( Rel R -> ( x `' R y <-> y R x ) )
9		relbrcnvg	|- ( Rel R -> ( y `' R x <-> x R y ) )
10	8 9	imbi12d	|- ( Rel R -> ( ( x `' R y -> y `' R x ) <-> ( y R x -> x R y ) ) )
11	10	2albidv	|- ( Rel R -> ( A. x A. y ( x `' R y -> y `' R x ) <-> A. x A. y ( y R x -> x R y ) ) )
12	7 11	bitrd	|- ( Rel R -> ( R C_ `' R <-> A. x A. y ( y R x -> x R y ) ) )
13	2 12	anbi12d	|- ( Rel R -> ( ( `' R C_ R /\ R C_ `' R ) <-> ( A. x A. y ( x R y -> y R x ) /\ A. x A. y ( y R x -> x R y ) ) ) )
14		eqss	|- ( `' R = R <-> ( `' R C_ R /\ R C_ `' R ) )
15		2albiim	|- ( A. x A. y ( x R y <-> y R x ) <-> ( A. x A. y ( x R y -> y R x ) /\ A. x A. y ( y R x -> x R y ) ) )
16	13 14 15	3bitr4g	|- ( Rel R -> ( `' R = R <-> A. x A. y ( x R y <-> y R x ) ) )