# Metamath Proof Explorer

## Theorem reldmmpo

Description: The domain of an operation defined by maps-to notation is a relation. (Contributed by Stefan O'Rear, 27-Nov-2014)

Ref Expression
Hypothesis rngop.1 ${⊢}{F}=\left({x}\in {A},{y}\in {B}⟼{C}\right)$
Assertion reldmmpo ${⊢}\mathrm{Rel}\mathrm{dom}{F}$

### Proof

Step Hyp Ref Expression
1 rngop.1 ${⊢}{F}=\left({x}\in {A},{y}\in {B}⟼{C}\right)$
2 reldmoprab ${⊢}\mathrm{Rel}\mathrm{dom}\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}={C}\right)\right\}$
3 df-mpo ${⊢}\left({x}\in {A},{y}\in {B}⟼{C}\right)=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}={C}\right)\right\}$
4 1 3 eqtri ${⊢}{F}=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}={C}\right)\right\}$
5 4 dmeqi ${⊢}\mathrm{dom}{F}=\mathrm{dom}\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}={C}\right)\right\}$
6 5 releqi ${⊢}\mathrm{Rel}\mathrm{dom}{F}↔\mathrm{Rel}\mathrm{dom}\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {A}\wedge {y}\in {B}\right)\wedge {z}={C}\right)\right\}$
7 2 6 mpbir ${⊢}\mathrm{Rel}\mathrm{dom}{F}$