Theorem opabssxp

Description: An abstraction relation is a subset of a related Cartesian product. (Contributed by NM, 16-Jul-1995)

	Ref	Expression
Assertion	opabssxp	$$⊢\left\{⟨x,y⟩|\left(\left(x\in A\wedge y\in B\right)\wedge \phi \right)\right\}\subseteq A\times B$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(\left(x\in A\wedge y\in B\right)\wedge \phi \right)\to \left(x\in A\wedge y\in B\right)$$
2	1	ssopab2i	$$⊢\left\{⟨x,y⟩|\left(\left(x\in A\wedge y\in B\right)\wedge \phi \right)\right\}\subseteq \left\{⟨x,y⟩|\left(x\in A\wedge y\in B\right)\right\}$$
3		df-xp	$$⊢A\times B=\left\{⟨x,y⟩|\left(x\in A\wedge y\in B\right)\right\}$$
4	2 3	sseqtrri	$$⊢\left\{⟨x,y⟩|\left(\left(x\in A\wedge y\in B\right)\wedge \phi \right)\right\}\subseteq A\times B$$