resopab2

Description: Restriction of a class abstraction of ordered pairs. (Contributed by NM, 24-Aug-2007)

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

Step	Hyp	Ref	Expression
1		resopab	$⊢ {\{⟨x, y⟩ \| (x \in B \land φ)\} ↾}_{A} = \{⟨x, y⟩ \| (x \in A \land (x \in B \land φ))\}$
2		ssel	$⊢ A \subseteq B \to (x \in A \to x \in B)$
3	2	pm4.71d	$⊢ A \subseteq B \to (x \in A \leftrightarrow (x \in A \land x \in B))$
4	3	anbi1d	$⊢ A \subseteq B \to ((x \in A \land φ) \leftrightarrow ((x \in A \land x \in B) \land φ))$
5		anass	$⊢ ((x \in A \land x \in B) \land φ) \leftrightarrow (x \in A \land (x \in B \land φ))$
6	4 5	bitr2di	$⊢ A \subseteq B \to ((x \in A \land (x \in B \land φ)) \leftrightarrow (x \in A \land φ))$
7	6	opabbidv	$⊢ A \subseteq B \to \{⟨x, y⟩ \| (x \in A \land (x \in B \land φ))\} = \{⟨x, y⟩ \| (x \in A \land φ)\}$
8	1 7	eqtrid	$⊢ A \subseteq B \to {\{⟨x, y⟩ \| (x \in B \land φ)\} ↾}_{A} = \{⟨x, y⟩ \| (x \in A \land φ)\}$

Metamath Proof Explorer