This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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