Theorem opelxp 4749

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 4737	. 2 |- ( <. A , B >. e. ( C X. D ) <-> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
2		vex 2802	. . . . . . 7 |- x e. _V
3		vex 2802	. . . . . . 7 |- y e. _V
4	2, 3	opth2 4326	. . . . . 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 3857	. . . . . 6 |- ( x = A -> <. x , y >. = <. A , y >. )
13	12	eqeq2d 2241	. . . . 5 |- ( x = A -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. A , y >. ) )
14		opeq2 3858	. . . . . 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 2922	. . . 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 3669   X. cxp 4717

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 4202  ax-pow 4258  ax-pr 4293

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 2801  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-opab 4146  df-xp 4725

This theorem is referenced by:  brxp  4750  opelxpi  4751  opelxp1  4753  opelxp2  4754  opthprc  4770  elxp3  4773  opeliunxp  4774  optocl  4795  xpiindim  4859  opelres  5010  resiexg  5050  restidsing  5061  codir  5117  qfto  5118  xpmlem  5149  rnxpid  5163  ssrnres  5171  dfco2  5228  relssdmrn  5249  ressn  5269  opelf  5496  fnovex  6034  oprab4  6075  resoprab  6100  elmpocl  6200  fo1stresm  6307  fo2ndresm  6308  dfoprab4  6338  xporderlem  6377  f1od2  6381  brecop  6772  xpdom2  6990  djulclb  7222  djuss  7237  enq0enq  7618  enq0sym  7619  enq0tr  7621  nqnq0pi  7625  nnnq0lem1  7633  elinp  7661  genipv  7696  prsrlem1  7929  gt0srpr  7935  opelcn  8013  opelreal  8014  elreal2  8017  frecuzrdgrrn  10630  frec2uzrdg  10631  frecuzrdgrcl  10632  frecuzrdgsuc  10636  frecuzrdgrclt  10637  frecuzrdgsuctlem  10645  fisumcom2  11949  fprodcom2fi  12137  sqpweven  12697  2sqpwodd  12698  phimullem  12747  relelbasov  13095  txuni2  14930  txcnp  14945  txcnmpt  14947  txdis1cn  14952  txlm  14953  xmeterval  15109  limccnp2lem  15350  limccnp2cntop  15351  lgsquadlem1  15756  lgsquadlem2  15757