Theorem opelxp 4751

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 4739	. 2 |- ( <. A , B >. e. ( C X. D ) <-> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
2		vex 2803	. . . . . . 7 |- x e. _V
3		vex 2803	. . . . . . 7 |- y e. _V
4	2, 3	opth2 4328	. . . . . 6 |- ( <. A , B >. = <. x , y >. <-> ( A = x /\ B = y ) )
5		eleq1 2292	. . . . . . 7 |- ( A = x -> ( A e. C <-> x e. C ) )
6		eleq1 2292	. . . . . . 7 |- ( B = y -> ( B e. D <-> y e. D ) )
7	5, 6	bi2anan9 608	. . . . . 6 |- ( ( A = x /\ B = y ) -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
8	4, 7	sylbi 121	. . . . 5 |- ( <. A , B >. = <. x , y >. -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
9	8	biimprcd 160	. . . 4 |- ( ( x e. C /\ y e. D ) -> ( <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) ) )
10	9	rexlimivv 2654	. . 3 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) )
11		eqid 2229	. . . 4 |- <. A , B >. = <. A , B >.
12		opeq1 3858	. . . . . 6 |- ( x = A -> <. x , y >. = <. A , y >. )
13	12	eqeq2d 2241	. . . . 5 |- ( x = A -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. A , y >. ) )
14		opeq2 3859	. . . . . 6 |- ( y = B -> <. A , y >. = <. A , B >. )
15	14	eqeq2d 2241	. . . . 5 |- ( y = B -> ( <. A , B >. = <. A , y >. <-> <. A , B >. = <. A , B >. ) )
16	13, 15	rspc2ev 2923	. . . 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 1360	. . 3 |- ( ( A e. C /\ B e. D ) -> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
18	10, 17	impbii 126	. 2 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. <-> ( A e. C /\ B e. D ) )
19	1, 18	bitri 184	1 |- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )

Syntax hints:   /\ wa 104   <-> wb 105   = wceq 1395   e. wcel 2200   E.wrex 2509   <.cop 3670   X. cxp 4719

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4203  ax-pow 4260  ax-pr 4295

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2802  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-opab 4147  df-xp 4727

This theorem is referenced by:  brxp  4752  opelxpi  4753  opelxp1  4755  opelxp2  4756  opthprc  4773  elxp3  4776  opeliunxp  4777  optocl  4798  xpiindim  4863  opelres  5014  resiexg  5054  restidsing  5065  codir  5121  qfto  5122  xpmlem  5153  rnxpid  5167  ssrnres  5175  dfco2  5232  relssdmrn  5253  ressn  5273  opelf  5502  fnovex  6044  oprab4  6085  resoprab  6110  elmpocl  6210  fo1stresm  6317  fo2ndresm  6318  dfoprab4  6348  xporderlem  6389  f1od2  6393  brecop  6787  xpdom2  7008  djulclb  7243  djuss  7258  enq0enq  7639  enq0sym  7640  enq0tr  7642  nqnq0pi  7646  nnnq0lem1  7654  elinp  7682  genipv  7717  prsrlem1  7950  gt0srpr  7956  opelcn  8034  opelreal  8035  elreal2  8038  frecuzrdgrrn  10658  frec2uzrdg  10659  frecuzrdgrcl  10660  frecuzrdgsuc  10664  frecuzrdgrclt  10665  frecuzrdgsuctlem  10673  fisumcom2  11986  fprodcom2fi  12174  sqpweven  12734  2sqpwodd  12735  phimullem  12784  relelbasov  13132  txuni2  14967  txcnp  14982  txcnmpt  14984  txdis1cn  14989  txlm  14990  xmeterval  15146  limccnp2lem  15387  limccnp2cntop  15388  lgsquadlem1  15793  lgsquadlem2  15794