Theorem rnoprab2

Description: The range of a restricted operation class abstraction. (Contributed by Scott Fenton, 21-Mar-2012)

	Ref	Expression
Assertion	rnoprab2	$$⊢\mathrm{ran}\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in A\wedge y\in B\right)\wedge \phi \right)\right\}=\left\{z|\exists x\in A\exists y\in B\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		rnoprab	$$⊢\mathrm{ran}\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in A\wedge y\in B\right)\wedge \phi \right)\right\}=\left\{z|\exists x\exists y\left(\left(x\in A\wedge y\in B\right)\wedge \phi \right)\right\}$$
2		r2ex	$$⊢\exists x\in A\exists y\in B\phi \leftrightarrow \exists x\exists y\left(\left(x\in A\wedge y\in B\right)\wedge \phi \right)$$
3	2	abbii	$$⊢\left\{z|\exists x\in A\exists y\in B\phi \right\}=\left\{z|\exists x\exists y\left(\left(x\in A\wedge y\in B\right)\wedge \phi \right)\right\}$$
4	1 3	eqtr4i	$$⊢\mathrm{ran}\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in A\wedge y\in B\right)\wedge \phi \right)\right\}=\left\{z|\exists x\in A\exists y\in B\phi \right\}$$