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	⊢ ( ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ 𝐴 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → ( 𝑥 𝐴 𝑥 ∧ 𝑦 𝐴 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		undmrnresiss	⊢ ( ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ 𝐴 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → ( 𝑥 𝐴 𝑥 ∧ 𝑦 𝐴 𝑦 ) ) )