Theorem elopg

Description: Characterization of the elements of an ordered pair. Closed form of elop . (Contributed by BJ, 22-Jun-2019) (Avoid depending on this detail.)

	Ref	Expression
Assertion	elopg	|- ( ( A e. V /\ B e. W ) -> ( C e. <. A , B >. <-> ( C = { A } \/ C = { A , B } ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfopg	|- ( ( A e. V /\ B e. W ) -> <. A , B >. = { { A } , { A , B } } )
2		eleq2	|- ( <. A , B >. = { { A } , { A , B } } -> ( C e. <. A , B >. <-> C e. { { A } , { A , B } } ) )
3		snex	|- { A } e. _V
4		prex	|- { A , B } e. _V
5	3 4	elpr2	|- ( C e. { { A } , { A , B } } <-> ( C = { A } \/ C = { A , B } ) )
6	2 5	bitrdi	|- ( <. A , B >. = { { A } , { A , B } } -> ( C e. <. A , B >. <-> ( C = { A } \/ C = { A , B } ) ) )
7	1 6	syl	|- ( ( A e. V /\ B e. W ) -> ( C e. <. A , B >. <-> ( C = { A } \/ C = { A , B } ) ) )