opabex

Description: Existence of a function expressed as class of ordered pairs. (Contributed by NM, 21-Jul-1996)

Step	Hyp	Ref	Expression
1		opabex.1	$⊢ A \in V$
2		opabex.2	$⊢ x \in A \to \exists^{*} y φ$
3		funopab	$⊢ Fun \{⟨x, y⟩ \| (x \in A \land φ)\} \leftrightarrow \forall x \exists^{*} y (x \in A \land φ)$
4		moanimv	$⊢ \exists^{} y (x \in A \land φ) \leftrightarrow (x \in A \to \exists^{} y φ)$
5	2 4	mpbir	$⊢ \exists^{*} y (x \in A \land φ)$
6	3 5	mpgbir	$⊢ Fun \{⟨x, y⟩ \| (x \in A \land φ)\}$
7		dmopabss	$⊢ dom \{⟨x, y⟩ \| (x \in A \land φ)\} \subseteq A$
8	1 7	ssexi	$⊢ dom \{⟨x, y⟩ \| (x \in A \land φ)\} \in V$
9		funex	$⊢ (Fun \{⟨x, y⟩ \| (x \in A \land φ)\} \land dom \{⟨x, y⟩ \| (x \in A \land φ)\} \in V) \to \{⟨x, y⟩ \| (x \in A \land φ)\} \in V$
10	6 8 9	mp2an	$⊢ \{⟨x, y⟩ \| (x \in A \land φ)\} \in V$

Metamath Proof Explorer