Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Relations
elrelscnveq4
Next ⟩
cnvelrels
Metamath Proof Explorer
Ascii
Unicode
Theorem
elrelscnveq4
Description:
Two ways of saying a relation is symmetric.
(Contributed by
Peter Mazsa
, 22-Aug-2021)
Ref
Expression
Assertion
elrelscnveq4
⊢
R
∈
Rels
→
R
-1
⊆
R
↔
∀
x
∀
y
x
R
y
↔
y
R
x
Proof
Step
Hyp
Ref
Expression
1
elrelscnveq
⊢
R
∈
Rels
→
R
-1
⊆
R
↔
R
-1
=
R
2
elrelscnveq2
⊢
R
∈
Rels
→
R
-1
=
R
↔
∀
x
∀
y
x
R
y
↔
y
R
x
3
1
2
bitrd
⊢
R
∈
Rels
→
R
-1
⊆
R
↔
∀
x
∀
y
x
R
y
↔
y
R
x