rnoprab

Description: The range of an operation class abstraction. (Contributed by NM, 30-Aug-2004) (Revised by David Abernethy, 19-Apr-2013)

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

Step	Hyp	Ref	Expression
1		dfoprab2	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\}$
2	1	rneqi	$⊢ ran \{⟨⟨x, y⟩, z⟩ \| φ\} = ran \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\}$
3		rnopab	$⊢ ran \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\} = \{z \| \exists w \exists x \exists y (w = ⟨x, y⟩ \land φ)\}$
4		exrot3	$⊢ \exists w \exists x \exists y (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y \exists w (w = ⟨x, y⟩ \land φ)$
5		opex	$⊢ ⟨x, y⟩ \in V$
6	5	isseti	$⊢ \exists w w = ⟨x, y⟩$
7		19.41v	$⊢ \exists w (w = ⟨x, y⟩ \land φ) \leftrightarrow (\exists w w = ⟨x, y⟩ \land φ)$
8	6 7	mpbiran	$⊢ \exists w (w = ⟨x, y⟩ \land φ) \leftrightarrow φ$
9	8	2exbii	$⊢ \exists x \exists y \exists w (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y φ$
10	4 9	bitri	$⊢ \exists w \exists x \exists y (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y φ$
11	10	abbii	$⊢ \{z \| \exists w \exists x \exists y (w = ⟨x, y⟩ \land φ)\} = \{z \| \exists x \exists y φ\}$
12	2 3 11	3eqtri	$⊢ ran \{⟨⟨x, y⟩, z⟩ \| φ\} = \{z \| \exists x \exists y φ\}$

Metamath Proof Explorer