This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem resoprab

Description: Restriction of an operation class abstraction. (Contributed by NM, 10-Feb-2007)

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

Proof

Step	Hyp	Ref	Expression
1		resopab	$⊢ {\{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\} ↾}_{(A \times B)} = \{⟨w, z⟩ \| (w \in (A \times B) \land \exists x \exists y (w = ⟨x, y⟩ \land φ))\}$
2		19.42vv	$⊢ \exists x \exists y (w \in (A \times B) \land (w = ⟨x, y⟩ \land φ)) \leftrightarrow (w \in (A \times B) \land \exists x \exists y (w = ⟨x, y⟩ \land φ))$
3		an12	$⊢ (w \in (A \times B) \land (w = ⟨x, y⟩ \land φ)) \leftrightarrow (w = ⟨x, y⟩ \land (w \in (A \times B) \land φ))$
4		eleq1	$⊢ w = ⟨x, y⟩ \to (w \in (A \times B) \leftrightarrow ⟨x, y⟩ \in (A \times B))$
5		opelxp	$⊢ ⟨x, y⟩ \in (A \times B) \leftrightarrow (x \in A \land y \in B)$
6	4 5	bitrdi	$⊢ w = ⟨x, y⟩ \to (w \in (A \times B) \leftrightarrow (x \in A \land y \in B))$
7	6	anbi1d	$⊢ w = ⟨x, y⟩ \to ((w \in (A \times B) \land φ) \leftrightarrow ((x \in A \land y \in B) \land φ))$
8	7	pm5.32i	$⊢ (w = ⟨x, y⟩ \land (w \in (A \times B) \land φ)) \leftrightarrow (w = ⟨x, y⟩ \land ((x \in A \land y \in B) \land φ))$
9	3 8	bitri	$⊢ (w \in (A \times B) \land (w = ⟨x, y⟩ \land φ)) \leftrightarrow (w = ⟨x, y⟩ \land ((x \in A \land y \in B) \land φ))$
10	9	2exbii	$⊢ \exists x \exists y (w \in (A \times B) \land (w = ⟨x, y⟩ \land φ)) \leftrightarrow \exists x \exists y (w = ⟨x, y⟩ \land ((x \in A \land y \in B) \land φ))$
11	2 10	bitr3i	$⊢ (w \in (A \times B) \land \exists x \exists y (w = ⟨x, y⟩ \land φ)) \leftrightarrow \exists x \exists y (w = ⟨x, y⟩ \land ((x \in A \land y \in B) \land φ))$
12	11	opabbii	$⊢ \{⟨w, z⟩ \| (w \in (A \times B) \land \exists x \exists y (w = ⟨x, y⟩ \land φ))\} = \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land ((x \in A \land y \in B) \land φ))\}$
13	1 12	eqtri	$⊢ {\{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\} ↾}_{(A \times B)} = \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land ((x \in A \land y \in B) \land φ))\}$
14		dfoprab2	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\}$
15	14	reseq1i	$⊢ {\{⟨⟨x, y⟩, z⟩ \| φ\} ↾}_{(A \times B)} = {\{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\} ↾}_{(A \times B)}$
16		dfoprab2	$⊢ \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land φ)\} = \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land ((x \in A \land y \in B) \land φ))\}$
17	13 15 16	3eqtr4i	$⊢ {\{⟨⟨x, y⟩, z⟩ \| φ\} ↾}_{(A \times B)} = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land φ)\}$