Description: For sets, being an element of the class of reflexive and symmetric relations is equivalent to satisfying the reflexive and symmetric relation predicates. (Contributed by Peter Mazsa, 23-Aug-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | elrefsymrelsrel |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elin | ||
2 | elrefrelsrel | ||
3 | elsymrelsrel | ||
4 | 2 3 | anbi12d | |
5 | 1 4 | syl5bb |