Theorem resopab

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

	Ref	Expression
Assertion	resopab	$$⊢{\left\{⟨x,y⟩|\phi \right\}\upharpoonright }_A=\left\{⟨x,y⟩|\left(x\in A\wedge \phi \right)\right\}$$

Proof

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