Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Preparatory theorems
relcnveq3
Next ⟩
relcnveq
Metamath Proof Explorer
Ascii
Unicode
Theorem
relcnveq3
Description:
Two ways of saying a relation is symmetric.
(Contributed by
FL
, 31-Aug-2009)
Ref
Expression
Assertion
relcnveq3
⊢
Rel
⁡
R
→
R
=
R
-1
↔
∀
x
∀
y
x
R
y
→
y
R
x
Proof
Step
Hyp
Ref
Expression
1
eqss
⊢
R
=
R
-1
↔
R
⊆
R
-1
∧
R
-1
⊆
R
2
cnvsym
⊢
R
-1
⊆
R
↔
∀
x
∀
y
x
R
y
→
y
R
x
3
2
biimpi
⊢
R
-1
⊆
R
→
∀
x
∀
y
x
R
y
→
y
R
x
4
3
a1d
⊢
R
-1
⊆
R
→
Rel
⁡
R
→
∀
x
∀
y
x
R
y
→
y
R
x
5
4
adantl
⊢
R
⊆
R
-1
∧
R
-1
⊆
R
→
Rel
⁡
R
→
∀
x
∀
y
x
R
y
→
y
R
x
6
5
com12
⊢
Rel
⁡
R
→
R
⊆
R
-1
∧
R
-1
⊆
R
→
∀
x
∀
y
x
R
y
→
y
R
x
7
dfrel2
⊢
Rel
⁡
R
↔
R
-1
-1
=
R
8
cnvss
⊢
R
-1
⊆
R
→
R
-1
-1
⊆
R
-1
9
sseq1
⊢
R
-1
-1
=
R
→
R
-1
-1
⊆
R
-1
↔
R
⊆
R
-1
10
8
9
syl5ibcom
⊢
R
-1
⊆
R
→
R
-1
-1
=
R
→
R
⊆
R
-1
11
2
10
sylbir
⊢
∀
x
∀
y
x
R
y
→
y
R
x
→
R
-1
-1
=
R
→
R
⊆
R
-1
12
11
com12
⊢
R
-1
-1
=
R
→
∀
x
∀
y
x
R
y
→
y
R
x
→
R
⊆
R
-1
13
7
12
sylbi
⊢
Rel
⁡
R
→
∀
x
∀
y
x
R
y
→
y
R
x
→
R
⊆
R
-1
14
2
biimpri
⊢
∀
x
∀
y
x
R
y
→
y
R
x
→
R
-1
⊆
R
15
13
14
jca2
⊢
Rel
⁡
R
→
∀
x
∀
y
x
R
y
→
y
R
x
→
R
⊆
R
-1
∧
R
-1
⊆
R
16
6
15
impbid
⊢
Rel
⁡
R
→
R
⊆
R
-1
∧
R
-1
⊆
R
↔
∀
x
∀
y
x
R
y
→
y
R
x
17
1
16
syl5bb
⊢
Rel
⁡
R
→
R
=
R
-1
↔
∀
x
∀
y
x
R
y
→
y
R
x