dmopab3

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

		Ref	Expression
	Assertion	dmopab3	$⊢ \forall x \in A \exists y φ \leftrightarrow dom \{⟨x, y⟩ \| (x \in A \land φ)\} = A$

Step	Hyp	Ref	Expression
1		df-ral	$⊢ \forall x \in A \exists y φ \leftrightarrow \forall x (x \in A \to \exists y φ)$
2		pm4.71	$⊢ (x \in A \to \exists y φ) \leftrightarrow (x \in A \leftrightarrow (x \in A \land \exists y φ))$
3	2	albii	$⊢ \forall x (x \in A \to \exists y φ) \leftrightarrow \forall x (x \in A \leftrightarrow (x \in A \land \exists y φ))$
4		dmopab	$⊢ dom \{⟨x, y⟩ \| (x \in A \land φ)\} = \{x \| \exists y (x \in A \land φ)\}$
5		19.42v	$⊢ \exists y (x \in A \land φ) \leftrightarrow (x \in A \land \exists y φ)$
6	5	abbii	$⊢ \{x \| \exists y (x \in A \land φ)\} = \{x \| (x \in A \land \exists y φ)\}$
7	4 6	eqtri	$⊢ dom \{⟨x, y⟩ \| (x \in A \land φ)\} = \{x \| (x \in A \land \exists y φ)\}$
8	7	eqeq1i	$⊢ dom \{⟨x, y⟩ \| (x \in A \land φ)\} = A \leftrightarrow \{x \| (x \in A \land \exists y φ)\} = A$
9		eqcom	$⊢ A = \{x \| (x \in A \land \exists y φ)\} \leftrightarrow \{x \| (x \in A \land \exists y φ)\} = A$
10		eqabb	$⊢ A = \{x \| (x \in A \land \exists y φ)\} \leftrightarrow \forall x (x \in A \leftrightarrow (x \in A \land \exists y φ))$
11	8 9 10	3bitr2ri	$⊢ \forall x (x \in A \leftrightarrow (x \in A \land \exists y φ)) \leftrightarrow dom \{⟨x, y⟩ \| (x \in A \land φ)\} = A$
12	1 3 11	3bitri	$⊢ \forall x \in A \exists y φ \leftrightarrow dom \{⟨x, y⟩ \| (x \in A \land φ)\} = A$

Metamath Proof Explorer