resopab

Description: Restriction of a class abstraction of ordered pairs. (Contributed by NM, 5-Nov-2002)

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

Step	Hyp	Ref	Expression
1		df-res	$⊢ {\{⟨x, y⟩ \| φ\} ↾}_{A} = \{⟨x, y⟩ \| φ\} \cap (A \times V)$
2		df-xp	$⊢ A \times V = \{⟨x, y⟩ \| (x \in A \land y \in V)\}$
3		vex	$⊢ y \in V$
4	3	biantru	$⊢ x \in A \leftrightarrow (x \in A \land y \in V)$
5	4	opabbii	$⊢ \{⟨x, y⟩ \| x \in A\} = \{⟨x, y⟩ \| (x \in A \land y \in V)\}$
6	2 5	eqtr4i	$⊢ A \times V = \{⟨x, y⟩ \| x \in A\}$
7	6	ineq2i	$⊢ \{⟨x, y⟩ \| φ\} \cap (A \times V) = \{⟨x, y⟩ \| φ\} \cap \{⟨x, y⟩ \| x \in A\}$
8		incom	$⊢ \{⟨x, y⟩ \| φ\} \cap \{⟨x, y⟩ \| x \in A\} = \{⟨x, y⟩ \| x \in A\} \cap \{⟨x, y⟩ \| φ\}$
9	7 8	eqtri	$⊢ \{⟨x, y⟩ \| φ\} \cap (A \times V) = \{⟨x, y⟩ \| x \in A\} \cap \{⟨x, y⟩ \| φ\}$
10		inopab	$⊢ \{⟨x, y⟩ \| x \in A\} \cap \{⟨x, y⟩ \| φ\} = \{⟨x, y⟩ \| (x \in A \land φ)\}$
11	9 10	eqtri	$⊢ \{⟨x, y⟩ \| φ\} \cap (A \times V) = \{⟨x, y⟩ \| (x \in A \land φ)\}$
12	1 11	eqtri	$⊢ {\{⟨x, y⟩ \| φ\} ↾}_{A} = \{⟨x, y⟩ \| (x \in A \land φ)\}$

Metamath Proof Explorer