dmopabss

Description: Upper bound for the domain of a restricted class of ordered pairs. (Contributed by NM, 31-Jan-2004)

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

Step	Hyp	Ref	Expression
1		dmopab	$⊢ dom \{⟨x, y⟩ \| (x \in A \land φ)\} = \{x \| \exists y (x \in A \land φ)\}$
2		19.42v	$⊢ \exists y (x \in A \land φ) \leftrightarrow (x \in A \land \exists y φ)$
3	2	abbii	$⊢ \{x \| \exists y (x \in A \land φ)\} = \{x \| (x \in A \land \exists y φ)\}$
4		ssab2	$⊢ \{x \| (x \in A \land \exists y φ)\} \subseteq A$
5	3 4	eqsstri	$⊢ \{x \| \exists y (x \in A \land φ)\} \subseteq A$
6	1 5	eqsstri	$⊢ dom \{⟨x, y⟩ \| (x \in A \land φ)\} \subseteq A$

Metamath Proof Explorer