Theorem opabssi

Description: Sufficient condition for a collection of ordered pairs to be a subclass of a relation. (Contributed by Peter Mazsa, 21-Oct-2019) (Revised by Thierry Arnoux, 18-Feb-2022)

	Ref	Expression
Hypothesis	opabssi.1	$$⊢\phi \to ⟨x,y⟩\in A$$
Assertion	opabssi	$$⊢\left\{⟨x,y⟩|\phi \right\}\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		opabssi.1	$$⊢\phi \to ⟨x,y⟩\in A$$
2		df-opab	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\right\}$$
3		eleq1	$$⊢z=⟨x,y⟩\to \left(z\in A\leftrightarrow ⟨x,y⟩\in A\right)$$
4	3	biimprd	$$⊢z=⟨x,y⟩\to \left(⟨x,y⟩\in A\to z\in A\right)$$
5	4 1	impel	$$⊢\left(z=⟨x,y⟩\wedge \phi \right)\to z\in A$$
6	5	exlimivv	$$⊢\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\to z\in A$$
7	6	abssi	$$⊢\left\{z|\exists x\exists y\left(z=⟨x,y⟩\wedge \phi \right)\right\}\subseteq A$$
8	2 7	eqsstri	$$⊢\left\{⟨x,y⟩|\phi \right\}\subseteq A$$