Metamath Proof Explorer

Theorem dfrefrel2

Description: Alternate definition of the reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021)

Ref Expression
Assertion dfrefrel2 ⊢ RefRel R ↔ I ∩ dom ⁡ R × ran ⁡ R ⊆ R ∧ Rel ⁡ R

Proof

Step Hyp Ref Expression
1 df-refrel ⊢ RefRel R ↔ I ∩ dom ⁡ R × ran ⁡ R ⊆ R ∩ dom ⁡ R × ran ⁡ R ∧ Rel ⁡ R
2 dfrel6 ⊢ Rel ⁡ R ↔ R ∩ dom ⁡ R × ran ⁡ R = R
3 2 biimpi ⊢ Rel ⁡ R → R ∩ dom ⁡ R × ran ⁡ R = R
4 3 sseq2d ⊢ Rel ⁡ R → I ∩ dom ⁡ R × ran ⁡ R ⊆ R ∩ dom ⁡ R × ran ⁡ R ↔ I ∩ dom ⁡ R × ran ⁡ R ⊆ R
5 4 pm5.32ri ⊢ I ∩ dom ⁡ R × ran ⁡ R ⊆ R ∩ dom ⁡ R × ran ⁡ R ∧ Rel ⁡ R ↔ I ∩ dom ⁡ R × ran ⁡ R ⊆ R ∧ Rel ⁡ R
6 1 5 bitri ⊢ RefRel R ↔ I ∩ dom ⁡ R × ran ⁡ R ⊆ R ∧ Rel ⁡ R