Theorem opelxp 4577

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 4565	. 2 |- ( <. A , B >. e. ( C X. D ) <-> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
2		vex 2692	. . . . . . 7 |- x e. _V
3		vex 2692	. . . . . . 7 |- y e. _V
4	2, 3	opth2 4170	. . . . . 6 |- ( <. A , B >. = <. x , y >. <-> ( A = x /\ B = y ) )
5		eleq1 2203	. . . . . . 7 |- ( A = x -> ( A e. C <-> x e. C ) )
6		eleq1 2203	. . . . . . 7 |- ( B = y -> ( B e. D <-> y e. D ) )
7	5, 6	bi2anan9 596	. . . . . 6 |- ( ( A = x /\ B = y ) -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
8	4, 7	sylbi 120	. . . . 5 |- ( <. A , B >. = <. x , y >. -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
9	8	biimprcd 159	. . . 4 |- ( ( x e. C /\ y e. D ) -> ( <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) ) )
10	9	rexlimivv 2558	. . 3 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) )
11		eqid 2140	. . . 4 |- <. A , B >. = <. A , B >.
12		opeq1 3713	. . . . . 6 |- ( x = A -> <. x , y >. = <. A , y >. )
13	12	eqeq2d 2152	. . . . 5 |- ( x = A -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. A , y >. ) )
14		opeq2 3714	. . . . . 6 |- ( y = B -> <. A , y >. = <. A , B >. )
15	14	eqeq2d 2152	. . . . 5 |- ( y = B -> ( <. A , B >. = <. A , y >. <-> <. A , B >. = <. A , B >. ) )
16	13, 15	rspc2ev 2808	. . . 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 1305	. . 3 |- ( ( A e. C /\ B e. D ) -> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
18	10, 17	impbii 125	. 2 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. <-> ( A e. C /\ B e. D ) )
19	1, 18	bitri 183	1 |- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )

Syntax hints:   /\ wa 103   <-> wb 104   = wceq 1332   e. wcel 1481   E.wrex 2418   <.cop 3535   X. cxp 4545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-pow 4106  ax-pr 4139

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-v 2691  df-un 3080  df-in 3082  df-ss 3089  df-pw 3517  df-sn 3538  df-pr 3539  df-op 3541  df-opab 3998  df-xp 4553

This theorem is referenced by:  brxp  4578  opelxpi  4579  opelxp1  4581  opelxp2  4582  opthprc  4598  elxp3  4601  opeliunxp  4602  optocl  4623  xpiindim  4684  opelres  4832  resiexg  4872  codir  4935  qfto  4936  xpmlem  4967  rnxpid  4981  ssrnres  4989  dfco2  5046  relssdmrn  5067  ressn  5087  opelf  5302  fnovex  5812  oprab4  5850  resoprab  5875  elmpocl  5976  fo1stresm  6067  fo2ndresm  6068  dfoprab4  6098  xporderlem  6136  f1od2  6140  brecop  6527  xpdom2  6733  djulclb  6948  djuss  6963  enq0enq  7263  enq0sym  7264  enq0tr  7266  nqnq0pi  7270  nnnq0lem1  7278  elinp  7306  genipv  7341  prsrlem1  7574  gt0srpr  7580  opelcn  7658  opelreal  7659  elreal2  7662  frecuzrdgrrn  10212  frec2uzrdg  10213  frecuzrdgrcl  10214  frecuzrdgsuc  10218  frecuzrdgrclt  10219  frecuzrdgsuctlem  10227  fisumcom2  11239  sqpweven  11889  2sqpwodd  11890  phimullem  11937  txuni2  12464  txcnp  12479  txcnmpt  12481  txdis1cn  12486  txlm  12487  xmeterval  12643  limccnp2lem  12853  limccnp2cntop  12854