This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elrefrels3

Description: Element of the class of reflexive relations. (Contributed by Peter Mazsa, 23-Jul-2019)

Ref Expression
Assertion elrefrels3 ( 𝑅 ∈ RefRels ↔ ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ∧ 𝑅 ∈ Rels ) )

Proof

Step Hyp Ref Expression
1 dfrefrels3 ⊢ RefRels = { 𝑟 ∈ Rels ∣ ∀ 𝑥 ∈ dom 𝑟 ∀ 𝑦 ∈ ran 𝑟 ( 𝑥 = 𝑦 → 𝑥 𝑟 𝑦 ) }
2 dmeq ⊢ ( 𝑟 = 𝑅 → dom 𝑟 = dom 𝑅 )
3 rneq ⊢ ( 𝑟 = 𝑅 → ran 𝑟 = ran 𝑅 )
4 breq ⊢ ( 𝑟 = 𝑅 → ( 𝑥 𝑟 𝑦 ↔ 𝑥 𝑅 𝑦 ) )
5 4 imbi2d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑥 = 𝑦 → 𝑥 𝑟 𝑦 ) ↔ ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ) )
6 3 5 raleqbidv ⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑦 ∈ ran 𝑟 ( 𝑥 = 𝑦 → 𝑥 𝑟 𝑦 ) ↔ ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ) )
7 2 6 raleqbidv ⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑥 ∈ dom 𝑟 ∀ 𝑦 ∈ ran 𝑟 ( 𝑥 = 𝑦 → 𝑥 𝑟 𝑦 ) ↔ ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ) )
8 1 7 rabeqel ⊢ ( 𝑅 ∈ RefRels ↔ ( ∀ 𝑥 ∈ dom 𝑅 ∀ 𝑦 ∈ ran 𝑅 ( 𝑥 = 𝑦 → 𝑥 𝑅 𝑦 ) ∧ 𝑅 ∈ Rels ) )