Metamath Proof Explorer

Theorem rabxp

Description: Class abstraction restricted to a Cartesian product as an ordered-pair class abstraction. (Contributed by NM, 20-Feb-2014)

		Ref	Expression
	Hypothesis	rabxp.1	$⊢ x = ⟨y, z⟩ \to (φ \leftrightarrow ψ)$
	Assertion	rabxp	$⊢ \{x \in (A \times B) \| φ\} = \{⟨y, z⟩ \| (y \in A \land z \in B \land ψ)\}$

Proof

Step	Hyp	Ref	Expression
1		rabxp.1	$⊢ x = ⟨y, z⟩ \to (φ \leftrightarrow ψ)$
2		elxp	$⊢ x \in (A \times B) \leftrightarrow \exists y \exists z (x = ⟨y, z⟩ \land (y \in A \land z \in B))$
3	2	anbi1i	$⊢ (x \in (A \times B) \land φ) \leftrightarrow (\exists y \exists z (x = ⟨y, z⟩ \land (y \in A \land z \in B)) \land φ)$
4		19.41vv	$⊢ \exists y \exists z ((x = ⟨y, z⟩ \land (y \in A \land z \in B)) \land φ) \leftrightarrow (\exists y \exists z (x = ⟨y, z⟩ \land (y \in A \land z \in B)) \land φ)$
5		anass	$⊢ ((x = ⟨y, z⟩ \land (y \in A \land z \in B)) \land φ) \leftrightarrow (x = ⟨y, z⟩ \land ((y \in A \land z \in B) \land φ))$
6	1	anbi2d	$⊢ x = ⟨y, z⟩ \to (((y \in A \land z \in B) \land φ) \leftrightarrow ((y \in A \land z \in B) \land ψ))$
7		df-3an	$⊢ (y \in A \land z \in B \land ψ) \leftrightarrow ((y \in A \land z \in B) \land ψ)$
8	6 7	bitr4di	$⊢ x = ⟨y, z⟩ \to (((y \in A \land z \in B) \land φ) \leftrightarrow (y \in A \land z \in B \land ψ))$
9	8	pm5.32i	$⊢ (x = ⟨y, z⟩ \land ((y \in A \land z \in B) \land φ)) \leftrightarrow (x = ⟨y, z⟩ \land (y \in A \land z \in B \land ψ))$
10	5 9	bitri	$⊢ ((x = ⟨y, z⟩ \land (y \in A \land z \in B)) \land φ) \leftrightarrow (x = ⟨y, z⟩ \land (y \in A \land z \in B \land ψ))$
11	10	2exbii	$⊢ \exists y \exists z ((x = ⟨y, z⟩ \land (y \in A \land z \in B)) \land φ) \leftrightarrow \exists y \exists z (x = ⟨y, z⟩ \land (y \in A \land z \in B \land ψ))$
12	3 4 11	3bitr2i	$⊢ (x \in (A \times B) \land φ) \leftrightarrow \exists y \exists z (x = ⟨y, z⟩ \land (y \in A \land z \in B \land ψ))$
13	12	abbii	$⊢ \{x \| (x \in (A \times B) \land φ)\} = \{x \| \exists y \exists z (x = ⟨y, z⟩ \land (y \in A \land z \in B \land ψ))\}$
14		df-rab	$⊢ \{x \in (A \times B) \| φ\} = \{x \| (x \in (A \times B) \land φ)\}$
15		df-opab	$⊢ \{⟨y, z⟩ \| (y \in A \land z \in B \land ψ)\} = \{x \| \exists y \exists z (x = ⟨y, z⟩ \land (y \in A \land z \in B \land ψ))\}$
16	13 14 15	3eqtr4i	$⊢ \{x \in (A \times B) \| φ\} = \{⟨y, z⟩ \| (y \in A \land z \in B \land ψ)\}$