Theorem opelxp

Description: Ordered pair membership in a Cartesian product. (Contributed by NM, 15-Nov-1994) (Proof shortened by Andrew Salmon, 12-Aug-2011) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Assertion	opelxp	|- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )

Proof

Step	Hyp	Ref	Expression
1		elxp2	|- ( <. A , B >. e. ( C X. D ) <-> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
2		vex	|- x e. _V
3		vex	|- y e. _V
4	2 3	opth2	|- ( <. A , B >. = <. x , y >. <-> ( A = x /\ B = y ) )
5		eleq1	|- ( A = x -> ( A e. C <-> x e. C ) )
6		eleq1	|- ( B = y -> ( B e. D <-> y e. D ) )
7	5 6	bi2anan9	|- ( ( A = x /\ B = y ) -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
8	4 7	sylbi	|- ( <. A , B >. = <. x , y >. -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
9	8	biimprcd	|- ( ( x e. C /\ y e. D ) -> ( <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) ) )
10	9	rexlimivv	|- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) )
11		eqid	|- <. A , B >. = <. A , B >.
12		opeq1	|- ( x = A -> <. x , y >. = <. A , y >. )
13	12	eqeq2d	|- ( x = A -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. A , y >. ) )
14		opeq2	|- ( y = B -> <. A , y >. = <. A , B >. )
15	14	eqeq2d	|- ( y = B -> ( <. A , B >. = <. A , y >. <-> <. A , B >. = <. A , B >. ) )
16	13 15	rspc2ev	|- ( ( A e. C /\ B e. D /\ <. A , B >. = <. A , B >. ) -> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
17	11 16	mp3an3	|- ( ( A e. C /\ B e. D ) -> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
18	10 17	impbii	|- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. <-> ( A e. C /\ B e. D ) )
19	1 18	bitri	|- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )