dmopab

Description: The domain of a class of ordered pairs. (Contributed by NM, 16-May-1995) (Revised by Mario Carneiro, 4-Dec-2016)

		Ref	Expression
	Assertion	dmopab	$⊢ dom \{⟨x, y⟩ \| φ\} = \{x \| \exists y φ\}$

Step	Hyp	Ref	Expression
1		nfopab1	$⊢ \underline{Ⅎ} x \{⟨x, y⟩ \| φ\}$
2		nfopab2	$⊢ \underline{Ⅎ} y \{⟨x, y⟩ \| φ\}$
3	1 2	dfdmf	$⊢ dom \{⟨x, y⟩ \| φ\} = \{x \| \exists y x \{⟨x, y⟩ \| φ\} y\}$
4		df-br	$⊢ x \{⟨x, y⟩ \| φ\} y \leftrightarrow ⟨x, y⟩ \in \{⟨x, y⟩ \| φ\}$
5		opabidw	$⊢ ⟨x, y⟩ \in \{⟨x, y⟩ \| φ\} \leftrightarrow φ$
6	4 5	bitri	$⊢ x \{⟨x, y⟩ \| φ\} y \leftrightarrow φ$
7	6	exbii	$⊢ \exists y x \{⟨x, y⟩ \| φ\} y \leftrightarrow \exists y φ$
8	7	abbii	$⊢ \{x \| \exists y x \{⟨x, y⟩ \| φ\} y\} = \{x \| \exists y φ\}$
9	3 8	eqtri	$⊢ dom \{⟨x, y⟩ \| φ\} = \{x \| \exists y φ\}$

Metamath Proof Explorer