Theorem reflexg

Description: Two ways of saying a relation is reflexive over its domain and range. (Contributed by RP, 4-Aug-2020)

	Ref	Expression
Assertion	reflexg	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\subseteq A\leftrightarrow \forall x\forall y\left(xAy\to \left(xAx\wedge yAy\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		undmrnresiss	$$⊢{\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}A\cup \mathrm{ran}A\right)}\subseteq A\leftrightarrow \forall x\forall y\left(xAy\to \left(xAx\wedge yAy\right)\right)$$