Theorem opelxp 4352

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

Assertion

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

Proof of Theorem opelxp

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp2 4341	. 2 |- ( <. A , B >. e. ( C X. D ) <-> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
2		vex 2557	. . . . . . 7 |- x e. _V
3		vex 2557	. . . . . . 7 |- y e. _V
4	2, 3	opth2 3974	. . . . . 6 |- ( <. A , B >. = <. x , y >. <-> ( A = x /\ B = y ) )
5		eleq1 2100	. . . . . . 7 |- ( A = x -> ( A e. C <-> x e. C ) )
6		eleq1 2100	. . . . . . 7 |- ( B = y -> ( B e. D <-> y e. D ) )
7	5, 6	bi2anan9 538	. . . . . 6 |- ( ( A = x /\ B = y ) -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
8	4, 7	sylbi 114	. . . . 5 |- ( <. A , B >. = <. x , y >. -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
9	8	biimprcd 149	. . . 4 |- ( ( x e. C /\ y e. D ) -> ( <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) ) )
10	9	rexlimivv 2435	. . 3 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) )
11		eqid 2040	. . . 4 |- <. A , B >. = <. A , B >.
12		opeq1 3546	. . . . . 6 |- ( x = A -> <. x , y >. = <. A , y >. )
13	12	eqeq2d 2051	. . . . 5 |- ( x = A -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. A , y >. ) )
14		opeq2 3547	. . . . . 6 |- ( y = B -> <. A , y >. = <. A , B >. )
15	14	eqeq2d 2051	. . . . 5 |- ( y = B -> ( <. A , B >. = <. A , y >. <-> <. A , B >. = <. A , B >. ) )
16	13, 15	rspc2ev 2661	. . . 4 |- ( ( 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 1221	. . 3 |- ( ( A e. C /\ B e. D ) -> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
18	10, 17	impbii 117	. 2 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. <-> ( A e. C /\ B e. D ) )
19	1, 18	bitri 173	1 |- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )

Syntax hints:   /\ wa 97   <-> wb 98   = wceq 1243   e. wcel 1393   E.wrex 2304   <.cop 3375   X. cxp 4321

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3872  ax-pow 3924  ax-pr 3941

This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2308  df-rex 2309  df-v 2556  df-un 2919  df-in 2921  df-ss 2928  df-pw 3358  df-sn 3378  df-pr 3379  df-op 3381  df-opab 3816  df-xp 4329

This theorem is referenced by:  brxp  4353  opelxpi  4354  opelxp1  4355  opelxp2  4356  opthprc  4369  elxp3  4372  opeliunxp  4373  optocl  4394  xpiindim  4451  opelres  4595  resiexg  4631  codir  4691  qfto  4692  xpmlem  4722  rnxpid  4733  ssrnres  4741  dfco2  4798  relssdmrn  4819  ressn  4836  opelf  5040  fnovex  5516  oprab4  5553  resoprab  5575  elmpt2cl  5676  fo1stresm  5766  fo2ndresm  5767  dfoprab4  5796  xporderlem  5830  brecop  6174  xpdom2  6283  enq0enq  6501  enq0sym  6502  enq0tr  6504  nqnq0pi  6508  nnnq0lem1  6516  elinp  6544  genipv  6579  prsrlem1  6799  gt0srpr  6805  opelcn  6875  opelreal  6876  elreal2  6879  frecuzrdgrrn  9063  frec2uzrdg  9064  frecuzrdgrom  9065  frecuzrdgsuc  9070