Metamath Proof Explorer

Theorem oprabrexex2

Description: Existence of an existentially restricted operation abstraction. (Contributed by Jeff Madsen, 11-Jun-2010)

		Ref	Expression
	Hypotheses	oprabrexex2.1	$⊢ A \in V$
		oprabrexex2.2	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} \in V$
	Assertion	oprabrexex2	$⊢ \{⟨⟨x, y⟩, z⟩ \| \exists w \in A φ\} \in V$

Proof

Step	Hyp	Ref	Expression
1		oprabrexex2.1	$⊢ A \in V$
2		oprabrexex2.2	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} \in V$
3		df-oprab	$⊢ \{⟨⟨x, y⟩, z⟩ \| \exists w \in A φ\} = \{v \| \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land \exists w \in A φ)\}$
4		rexcom4	$⊢ \exists w \in A \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow \exists x \exists w \in A \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ)$
5		rexcom4	$⊢ \exists w \in A \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow \exists y \exists w \in A \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ)$
6		rexcom4	$⊢ \exists w \in A \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow \exists z \exists w \in A (v = ⟨⟨x, y⟩, z⟩ \land φ)$
7		r19.42v	$⊢ \exists w \in A (v = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow (v = ⟨⟨x, y⟩, z⟩ \land \exists w \in A φ)$
8	7	exbii	$⊢ \exists z \exists w \in A (v = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow \exists z (v = ⟨⟨x, y⟩, z⟩ \land \exists w \in A φ)$
9	6 8	bitri	$⊢ \exists w \in A \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow \exists z (v = ⟨⟨x, y⟩, z⟩ \land \exists w \in A φ)$
10	9	exbii	$⊢ \exists y \exists w \in A \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land \exists w \in A φ)$
11	5 10	bitri	$⊢ \exists w \in A \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land \exists w \in A φ)$
12	11	exbii	$⊢ \exists x \exists w \in A \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ) \leftrightarrow \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land \exists w \in A φ)$
13	4 12	bitr2i	$⊢ \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land \exists w \in A φ) \leftrightarrow \exists w \in A \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ)$
14	13	abbii	$⊢ \{v \| \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land \exists w \in A φ)\} = \{v \| \exists w \in A \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ)\}$
15	3 14	eqtri	$⊢ \{⟨⟨x, y⟩, z⟩ \| \exists w \in A φ\} = \{v \| \exists w \in A \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ)\}$
16		df-oprab	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{v \| \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ)\}$
17	16 2	eqeltrri	$⊢ \{v \| \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ)\} \in V$
18	1 17	abrexex2	$⊢ \{v \| \exists w \in A \exists x \exists y \exists z (v = ⟨⟨x, y⟩, z⟩ \land φ)\} \in V$
19	15 18	eqeltri	$⊢ \{⟨⟨x, y⟩, z⟩ \| \exists w \in A φ\} \in V$