Theorem opabbrex

Description: A collection of ordered pairs with an extension of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by BJ/AV, 20-Jun-2019) (Proof shortened by OpenAI, 25-Mar-2020)

	Ref	Expression
Assertion	opabbrex	|- ( ( A. x A. y ( x R y -> ph ) /\ { <. x , y >. | ph } e. V ) -> { <. x , y >. | ( x R y /\ ps ) } e. _V )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( A. x A. y ( x R y -> ph ) /\ { <. x , y >. | ph } e. V ) -> { <. x , y >. | ph } e. V )
2		pm3.41	|- ( ( x R y -> ph ) -> ( ( x R y /\ ps ) -> ph ) )
3	2	2alimi	|- ( A. x A. y ( x R y -> ph ) -> A. x A. y ( ( x R y /\ ps ) -> ph ) )
4	3	adantr	|- ( ( A. x A. y ( x R y -> ph ) /\ { <. x , y >. | ph } e. V ) -> A. x A. y ( ( x R y /\ ps ) -> ph ) )
5		ssopab2	|- ( A. x A. y ( ( x R y /\ ps ) -> ph ) -> { <. x , y >. | ( x R y /\ ps ) } C_ { <. x , y >. | ph } )
6	4 5	syl	|- ( ( A. x A. y ( x R y -> ph ) /\ { <. x , y >. | ph } e. V ) -> { <. x , y >. | ( x R y /\ ps ) } C_ { <. x , y >. | ph } )
7	1 6	ssexd	|- ( ( A. x A. y ( x R y -> ph ) /\ { <. x , y >. | ph } e. V ) -> { <. x , y >. | ( x R y /\ ps ) } e. _V )