opabdm

Description: Domain of an ordered-pair class abstraction. (Contributed by Thierry Arnoux, 31-Aug-2017)

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

Step	Hyp	Ref	Expression
1		df-dm	$⊢ dom R = \{x \| \exists y x R y\}$
2		nfopab1	$⊢ \underline{Ⅎ} x \{⟨x, y⟩ \| φ\}$
3	2	nfeq2	$⊢ Ⅎ x R = \{⟨x, y⟩ \| φ\}$
4		nfopab2	$⊢ \underline{Ⅎ} y \{⟨x, y⟩ \| φ\}$
5	4	nfeq2	$⊢ Ⅎ y R = \{⟨x, y⟩ \| φ\}$
6		df-br	$⊢ x R y \leftrightarrow ⟨x, y⟩ \in R$
7		eleq2	$⊢ R = \{⟨x, y⟩ \| φ\} \to (⟨x, y⟩ \in R \leftrightarrow ⟨x, y⟩ \in \{⟨x, y⟩ \| φ\})$
8		opabidw	$⊢ ⟨x, y⟩ \in \{⟨x, y⟩ \| φ\} \leftrightarrow φ$
9	7 8	bitrdi	$⊢ R = \{⟨x, y⟩ \| φ\} \to (⟨x, y⟩ \in R \leftrightarrow φ)$
10	6 9	bitrid	$⊢ R = \{⟨x, y⟩ \| φ\} \to (x R y \leftrightarrow φ)$
11	5 10	exbid	$⊢ R = \{⟨x, y⟩ \| φ\} \to (\exists y x R y \leftrightarrow \exists y φ)$
12	3 11	abbid	$⊢ R = \{⟨x, y⟩ \| φ\} \to \{x \| \exists y x R y\} = \{x \| \exists y φ\}$
13	1 12	eqtrid	$⊢ R = \{⟨x, y⟩ \| φ\} \to dom R = \{x \| \exists y φ\}$

Metamath Proof Explorer