dmoprab

Description: The domain of an operation class abstraction. (Contributed by NM, 17-Mar-1995) (Revised by David Abernethy, 19-Jun-2012)

		Ref	Expression
	Assertion	dmoprab	$⊢ dom \{⟨⟨x, y⟩, z⟩ \| φ\} = \{⟨x, y⟩ \| \exists z φ\}$

Step	Hyp	Ref	Expression
1		dfoprab2	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\}$
2	1	dmeqi	$⊢ dom \{⟨⟨x, y⟩, z⟩ \| φ\} = dom \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\}$
3		dmopab	$⊢ dom \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\} = \{w \| \exists z \exists x \exists y (w = ⟨x, y⟩ \land φ)\}$
4		exrot3	$⊢ \exists z \exists x \exists y (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y \exists z (w = ⟨x, y⟩ \land φ)$
5		19.42v	$⊢ \exists z (w = ⟨x, y⟩ \land φ) \leftrightarrow (w = ⟨x, y⟩ \land \exists z φ)$
6	5	2exbii	$⊢ \exists x \exists y \exists z (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y (w = ⟨x, y⟩ \land \exists z φ)$
7	4 6	bitri	$⊢ \exists z \exists x \exists y (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y (w = ⟨x, y⟩ \land \exists z φ)$
8	7	abbii	$⊢ \{w \| \exists z \exists x \exists y (w = ⟨x, y⟩ \land φ)\} = \{w \| \exists x \exists y (w = ⟨x, y⟩ \land \exists z φ)\}$
9		df-opab	$⊢ \{⟨x, y⟩ \| \exists z φ\} = \{w \| \exists x \exists y (w = ⟨x, y⟩ \land \exists z φ)\}$
10	8 9	eqtr4i	$⊢ \{w \| \exists z \exists x \exists y (w = ⟨x, y⟩ \land φ)\} = \{⟨x, y⟩ \| \exists z φ\}$
11	2 3 10	3eqtri	$⊢ dom \{⟨⟨x, y⟩, z⟩ \| φ\} = \{⟨x, y⟩ \| \exists z φ\}$

Metamath Proof Explorer