rnoprab2

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

		Ref	Expression
	Assertion	rnoprab2	$⊢ ran \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land φ)\} = \{z \| \exists x \in A \exists y \in B φ\}$

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

Metamath Proof Explorer