Theorem opelopab4

Description: Ordered pair membership in a class abstraction of ordered pairs. Compare to elopab . (Contributed by Alan Sare, 8-Feb-2014) (Revised by Mario Carneiro, 6-May-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	opelopab4	|- ( <. u , v >. e. { <. x , y >. | ph } <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) )

Proof

Step	Hyp	Ref	Expression
1		elopab	|- ( <. u , v >. e. { <. x , y >. | ph } <-> E. x E. y ( <. u , v >. = <. x , y >. /\ ph ) )
2		vex	|- x e. _V
3		vex	|- y e. _V
4	2 3	opth	|- ( <. x , y >. = <. u , v >. <-> ( x = u /\ y = v ) )
5		eqcom	|- ( <. x , y >. = <. u , v >. <-> <. u , v >. = <. x , y >. )
6	4 5	bitr3i	|- ( ( x = u /\ y = v ) <-> <. u , v >. = <. x , y >. )
7	6	anbi1i	|- ( ( ( x = u /\ y = v ) /\ ph ) <-> ( <. u , v >. = <. x , y >. /\ ph ) )
8	7	2exbii	|- ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) <-> E. x E. y ( <. u , v >. = <. x , y >. /\ ph ) )
9	1 8	bitr4i	|- ( <. u , v >. e. { <. x , y >. | ph } <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) )