Theorem reldmoprab

Description: The domain of an operation class abstraction is a relation. (Contributed by NM, 17-Mar-1995)

	Ref	Expression
Assertion	reldmoprab	$$⊢\mathrm{Rel}\mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		dmoprab	$$⊢\mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}=\left\{⟨x,y⟩|\exists z\phi \right\}$$
2	1	relopabiv	$$⊢\mathrm{Rel}\mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$