This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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