Theorem dfrefrels3

Description: Alternate definition of the class of reflexive relations. (Contributed by Peter Mazsa, 8-Jul-2019)

	Ref	Expression
Assertion	dfrefrels3	⊢ RefRels = { 𝑟 ∈ Rels ∣ ∀ 𝑥 ∈ dom 𝑟 ∀ 𝑦 ∈ ran 𝑟 ( 𝑥 = 𝑦 → 𝑥 𝑟 𝑦 ) }

Proof

Step	Hyp	Ref	Expression
1		dfrefrels2	⊢ RefRels = { 𝑟 ∈ Rels ∣ ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 }
2		idinxpss	⊢ ( ( I ∩ ( dom 𝑟 × ran 𝑟 ) ) ⊆ 𝑟 ↔ ∀ 𝑥 ∈ dom 𝑟 ∀ 𝑦 ∈ ran 𝑟 ( 𝑥 = 𝑦 → 𝑥 𝑟 𝑦 ) )
3	1 2	rabbieq	⊢ RefRels = { 𝑟 ∈ Rels ∣ ∀ 𝑥 ∈ dom 𝑟 ∀ 𝑦 ∈ ran 𝑟 ( 𝑥 = 𝑦 → 𝑥 𝑟 𝑦 ) }