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 = (x \in A, y \in B ⟼ C)$
	Assertion	reldmmpo	$⊢ Rel dom F$

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

Metamath Proof Explorer