Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Symmetry
elsymrels5
Next ⟩
elsymrelsrel
Metamath Proof Explorer
Ascii
Unicode
Theorem
elsymrels5
Description:
Element of the class of symmetric relations.
(Contributed by
Peter Mazsa
, 17-Aug-2021)
Ref
Expression
Assertion
elsymrels5
⊢
R
∈
SymRels
↔
∀
x
∀
y
x
R
y
↔
y
R
x
∧
R
∈
Rels
Proof
Step
Hyp
Ref
Expression
1
dfsymrels5
⊢
SymRels
=
r
∈
Rels
|
∀
x
∀
y
x
r
y
↔
y
r
x
2
breq
⊢
r
=
R
→
x
r
y
↔
x
R
y
3
breq
⊢
r
=
R
→
y
r
x
↔
y
R
x
4
2
3
bibi12d
⊢
r
=
R
→
x
r
y
↔
y
r
x
↔
x
R
y
↔
y
R
x
5
4
2albidv
⊢
r
=
R
→
∀
x
∀
y
x
r
y
↔
y
r
x
↔
∀
x
∀
y
x
R
y
↔
y
R
x
6
1
5
rabeqel
⊢
R
∈
SymRels
↔
∀
x
∀
y
x
R
y
↔
y
R
x
∧
R
∈
Rels