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

Metamath Proof Explorer

Theorem dfrel6

Description: Alternate definition of the relation predicate. (Contributed by Peter Mazsa, 14-Mar-2019)

Ref Expression
Assertion dfrel6 ⊢ Rel ⁡ R ↔ R ∩ dom ⁡ R × ran ⁡ R = R

Proof

Step Hyp Ref Expression
1 dfrel5 ⊢ Rel ⁡ R ↔ R ↾ dom ⁡ R = R
2 dfres3 ⊢ R ↾ dom ⁡ R = R ∩ dom ⁡ R × ran ⁡ R
3 2 eqeq1i ⊢ R ↾ dom ⁡ R = R ↔ R ∩ dom ⁡ R × ran ⁡ R = R
4 1 3 bitri ⊢ Rel ⁡ R ↔ R ∩ dom ⁡ R × ran ⁡ R = R