Theorem opelxp 4723

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 4711	. 2 |- ( <. A , B >. e. ( C X. D ) <-> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
2		vex 2779	. . . . . . 7 |- x e. _V
3		vex 2779	. . . . . . 7 |- y e. _V
4	2, 3	opth2 4302	. . . . . 6 |- ( <. A , B >. = <. x , y >. <-> ( A = x /\ B = y ) )
5		eleq1 2270	. . . . . . 7 |- ( A = x -> ( A e. C <-> x e. C ) )
6		eleq1 2270	. . . . . . 7 |- ( B = y -> ( B e. D <-> y e. D ) )
7	5, 6	bi2anan9 606	. . . . . 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 2631	. . 3 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) )
11		eqid 2207	. . . 4 |- <. A , B >. = <. A , B >.
12		opeq1 3833	. . . . . 6 |- ( x = A -> <. x , y >. = <. A , y >. )
13	12	eqeq2d 2219	. . . . 5 |- ( x = A -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. A , y >. ) )
14		opeq2 3834	. . . . . 6 |- ( y = B -> <. A , y >. = <. A , B >. )
15	14	eqeq2d 2219	. . . . 5 |- ( y = B -> ( <. A , B >. = <. A , y >. <-> <. A , B >. = <. A , B >. ) )
16	13, 15	rspc2ev 2899	. . . 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 1339	. . 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 1373   e. wcel 2178   E.wrex 2487   <.cop 3646   X. cxp 4691

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2181  ax-ext 2189  ax-sep 4178  ax-pow 4234  ax-pr 4269

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-v 2778  df-un 3178  df-in 3180  df-ss 3187  df-pw 3628  df-sn 3649  df-pr 3650  df-op 3652  df-opab 4122  df-xp 4699

This theorem is referenced by:  brxp  4724  opelxpi  4725  opelxp1  4727  opelxp2  4728  opthprc  4744  elxp3  4747  opeliunxp  4748  optocl  4769  xpiindim  4833  opelres  4983  resiexg  5023  restidsing  5034  codir  5090  qfto  5091  xpmlem  5122  rnxpid  5136  ssrnres  5144  dfco2  5201  relssdmrn  5222  ressn  5242  opelf  5468  fnovex  6000  oprab4  6039  resoprab  6064  elmpocl  6164  fo1stresm  6270  fo2ndresm  6271  dfoprab4  6301  xporderlem  6340  f1od2  6344  brecop  6735  xpdom2  6951  djulclb  7183  djuss  7198  enq0enq  7579  enq0sym  7580  enq0tr  7582  nqnq0pi  7586  nnnq0lem1  7594  elinp  7622  genipv  7657  prsrlem1  7890  gt0srpr  7896  opelcn  7974  opelreal  7975  elreal2  7978  frecuzrdgrrn  10590  frec2uzrdg  10591  frecuzrdgrcl  10592  frecuzrdgsuc  10596  frecuzrdgrclt  10597  frecuzrdgsuctlem  10605  fisumcom2  11864  fprodcom2fi  12052  sqpweven  12612  2sqpwodd  12613  phimullem  12662  relelbasov  13009  txuni2  14843  txcnp  14858  txcnmpt  14860  txdis1cn  14865  txlm  14866  xmeterval  15022  limccnp2lem  15263  limccnp2cntop  15264  lgsquadlem1  15669  lgsquadlem2  15670