oprabex

Description: Existence of an operation class abstraction. (Contributed by NM, 19-Oct-2004)

Step	Hyp	Ref	Expression
1		oprabex.1	$⊢ A \in V$
2		oprabex.2	$⊢ B \in V$
3		oprabex.3	$⊢ (x \in A \land y \in B) \to \exists^{*} z φ$
4		oprabex.4	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land φ)\}$
5		moanimv	$⊢ \exists^{} z ((x \in A \land y \in B) \land φ) \leftrightarrow ((x \in A \land y \in B) \to \exists^{} z φ)$
6	3 5	mpbir	$⊢ \exists^{*} z ((x \in A \land y \in B) \land φ)$
7	6	funoprab	$⊢ Fun \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land φ)\}$
8	1 2	xpex	$⊢ A \times B \in V$
9		dmoprabss	$⊢ dom \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land φ)\} \subseteq A \times B$
10	8 9	ssexi	$⊢ dom \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land φ)\} \in V$
11		funex	$⊢ (Fun \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land φ)\} \land dom \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land φ)\} \in V) \to \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land φ)\} \in V$
12	7 10 11	mp2an	$⊢ \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land φ)\} \in V$
13	4 12	eqeltri	$⊢ F \in V$

Metamath Proof Explorer