elrefsymrels3

Description: Elements of the class of reflexive relations which are elements of the class of symmetric relations as well (like the elements of the class of equivalence relations dfeqvrels3 ) can use the A. x e. dom R x R x version for their reflexive part, not just the A. x e. dom R A. y e. ran R ( x = y -> x R y ) version of dfrefrels3 , cf. the comment of dfrefrel3 . (Contributed by Peter Mazsa, 22-Jul-2019) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	elrefsymrels3	$⊢ R \in (RefRels \cap SymRels) \leftrightarrow ((\forall x \in dom R x R x \land \forall x \forall y (x R y \to y R x)) \land R \in Rels)$

Proof

Step	Hyp	Ref	Expression
1		elrefsymrels2	$⊢ R \in (RefRels \cap SymRels) \leftrightarrow (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R) \land R \in Rels)$
2		idrefALT	$⊢ {I ↾}_{dom R} \subseteq R \leftrightarrow \forall x \in dom R x R x$
3		cnvsym	$⊢ R^{-1} \subseteq R \leftrightarrow \forall x \forall y (x R y \to y R x)$
4	2 3	anbi12i	$⊢ ({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R) \leftrightarrow (\forall x \in dom R x R x \land \forall x \forall y (x R y \to y R x))$
5	4	anbi1i	$⊢ (({I ↾}_{dom R} \subseteq R \land R^{-1} \subseteq R) \land R \in Rels) \leftrightarrow ((\forall x \in dom R x R x \land \forall x \forall y (x R y \to y R x)) \land R \in Rels)$
6	1 5	bitri	$⊢ R \in (RefRels \cap SymRels) \leftrightarrow ((\forall x \in dom R x R x \land \forall x \forall y (x R y \to y R x)) \land R \in Rels)$

Metamath Proof Explorer

Theorem elrefsymrels3

Proof