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	|- ( ph -> <. x , y >. e. A )
Assertion	opabssi	|- { <. x , y >. | ph } C_ A

Proof

Step	Hyp	Ref	Expression
1		opabssi.1	|- ( ph -> <. x , y >. e. A )
2		df-opab	|- { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
3		eleq1	|- ( z = <. x , y >. -> ( z e. A <-> <. x , y >. e. A ) )
4	3	biimprd	|- ( z = <. x , y >. -> ( <. x , y >. e. A -> z e. A ) )
5	4 1	impel	|- ( ( z = <. x , y >. /\ ph ) -> z e. A )
6	5	exlimivv	|- ( E. x E. y ( z = <. x , y >. /\ ph ) -> z e. A )
7	6	abssi	|- { z | E. x E. y ( z = <. x , y >. /\ ph ) } C_ A
8	2 7	eqsstri	|- { <. x , y >. | ph } C_ A