Metamath Proof Explorer

Theorem oprab4

Description: Two ways to state the domain of an operation. (Contributed by FL, 24-Jan-2010)

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

Step	Hyp	Ref	Expression
1		opelxp	$⊢ ⟨x, y⟩ \in (A \times B) \leftrightarrow (x \in A \land y \in B)$
2	1	anbi1i	$⊢ (⟨x, y⟩ \in (A \times B) \land φ) \leftrightarrow ((x \in A \land y \in B) \land φ)$
3	2	oprabbii	$⊢ \{⟨⟨x, y⟩, z⟩ \| (⟨x, y⟩ \in (A \times B) \land φ)\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land φ)\}$