Theorem opelxp 4613

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 4601	. 2 |- ( <. A , B >. e. ( C X. D ) <-> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
2		vex 2715	. . . . . . 7 |- x e. _V
3		vex 2715	. . . . . . 7 |- y e. _V
4	2, 3	opth2 4199	. . . . . 6 |- ( <. A , B >. = <. x , y >. <-> ( A = x /\ B = y ) )
5		eleq1 2220	. . . . . . 7 |- ( A = x -> ( A e. C <-> x e. C ) )
6		eleq1 2220	. . . . . . 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 2580	. . 3 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) )
11		eqid 2157	. . . 4 |- <. A , B >. = <. A , B >.
12		opeq1 3741	. . . . . 6 |- ( x = A -> <. x , y >. = <. A , y >. )
13	12	eqeq2d 2169	. . . . 5 |- ( x = A -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. A , y >. ) )
14		opeq2 3742	. . . . . 6 |- ( y = B -> <. A , y >. = <. A , B >. )
15	14	eqeq2d 2169	. . . . 5 |- ( y = B -> ( <. A , B >. = <. A , y >. <-> <. A , B >. = <. A , B >. ) )
16	13, 15	rspc2ev 2831	. . . 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 1308	. . 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 1335   e. wcel 2128   E.wrex 2436   <.cop 3563   X. cxp 4581

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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4134  ax-pr 4168

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-opab 4026  df-xp 4589

This theorem is referenced by:  brxp  4614  opelxpi  4615  opelxp1  4617  opelxp2  4618  opthprc  4634  elxp3  4637  opeliunxp  4638  optocl  4659  xpiindim  4720  opelres  4868  resiexg  4908  codir  4971  qfto  4972  xpmlem  5003  rnxpid  5017  ssrnres  5025  dfco2  5082  relssdmrn  5103  ressn  5123  opelf  5338  fnovex  5848  oprab4  5886  resoprab  5911  elmpocl  6012  fo1stresm  6103  fo2ndresm  6104  dfoprab4  6134  xporderlem  6172  f1od2  6176  brecop  6563  xpdom2  6769  djulclb  6989  djuss  7004  enq0enq  7334  enq0sym  7335  enq0tr  7337  nqnq0pi  7341  nnnq0lem1  7349  elinp  7377  genipv  7412  prsrlem1  7645  gt0srpr  7651  opelcn  7729  opelreal  7730  elreal2  7733  frecuzrdgrrn  10289  frec2uzrdg  10290  frecuzrdgrcl  10291  frecuzrdgsuc  10295  frecuzrdgrclt  10296  frecuzrdgsuctlem  10304  fisumcom2  11317  fprodcom2fi  11505  sqpweven  12029  2sqpwodd  12030  phimullem  12077  txuni2  12616  txcnp  12631  txcnmpt  12633  txdis1cn  12638  txlm  12639  xmeterval  12795  limccnp2lem  13005  limccnp2cntop  13006