dmoprabss

Description: The domain of an operation class abstraction. (Contributed by NM, 24-Aug-1995)

		Ref	Expression
	Assertion	dmoprabss	$⊢ dom \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land φ)\} \subseteq A \times B$

Step	Hyp	Ref	Expression
1		dmoprab	$⊢ dom \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land φ)\} = \{⟨x, y⟩ \| \exists z ((x \in A \land y \in B) \land φ)\}$
2		19.42v	$⊢ \exists z ((x \in A \land y \in B) \land φ) \leftrightarrow ((x \in A \land y \in B) \land \exists z φ)$
3	2	opabbii	$⊢ \{⟨x, y⟩ \| \exists z ((x \in A \land y \in B) \land φ)\} = \{⟨x, y⟩ \| ((x \in A \land y \in B) \land \exists z φ)\}$
4		opabssxp	$⊢ \{⟨x, y⟩ \| ((x \in A \land y \in B) \land \exists z φ)\} \subseteq A \times B$
5	3 4	eqsstri	$⊢ \{⟨x, y⟩ \| \exists z ((x \in A \land y \in B) \land φ)\} \subseteq A \times B$
6	1 5	eqsstri	$⊢ dom \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land φ)\} \subseteq A \times B$

Metamath Proof Explorer