Theorem opelxp 4569

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 4557	. 2 |- ( <. A , B >. e. ( C X. D ) <-> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
2		vex 2689	. . . . . . 7 |- x e. _V
3		vex 2689	. . . . . . 7 |- y e. _V
4	2, 3	opth2 4162	. . . . . 6 |- ( <. A , B >. = <. x , y >. <-> ( A = x /\ B = y ) )
5		eleq1 2202	. . . . . . 7 |- ( A = x -> ( A e. C <-> x e. C ) )
6		eleq1 2202	. . . . . . 7 |- ( B = y -> ( B e. D <-> y e. D ) )
7	5, 6	bi2anan9 595	. . . . . 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 2555	. . 3 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) )
11		eqid 2139	. . . 4 |- <. A , B >. = <. A , B >.
12		opeq1 3705	. . . . . 6 |- ( x = A -> <. x , y >. = <. A , y >. )
13	12	eqeq2d 2151	. . . . 5 |- ( x = A -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. A , y >. ) )
14		opeq2 3706	. . . . . 6 |- ( y = B -> <. A , y >. = <. A , B >. )
15	14	eqeq2d 2151	. . . . 5 |- ( y = B -> ( <. A , B >. = <. A , y >. <-> <. A , B >. = <. A , B >. ) )
16	13, 15	rspc2ev 2804	. . . 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 1304	. . 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 1331   e. wcel 1480   E.wrex 2417   <.cop 3530   X. cxp 4537

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-pow 4098  ax-pr 4131

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rex 2422  df-v 2688  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-opab 3990  df-xp 4545

This theorem is referenced by:  brxp  4570  opelxpi  4571  opelxp1  4573  opelxp2  4574  opthprc  4590  elxp3  4593  opeliunxp  4594  optocl  4615  xpiindim  4676  opelres  4824  resiexg  4864  codir  4927  qfto  4928  xpmlem  4959  rnxpid  4973  ssrnres  4981  dfco2  5038  relssdmrn  5059  ressn  5079  opelf  5294  fnovex  5804  oprab4  5842  resoprab  5867  elmpocl  5968  fo1stresm  6059  fo2ndresm  6060  dfoprab4  6090  xporderlem  6128  f1od2  6132  brecop  6519  xpdom2  6725  djulclb  6940  djuss  6955  enq0enq  7239  enq0sym  7240  enq0tr  7242  nqnq0pi  7246  nnnq0lem1  7254  elinp  7282  genipv  7317  prsrlem1  7550  gt0srpr  7556  opelcn  7634  opelreal  7635  elreal2  7638  frecuzrdgrrn  10181  frec2uzrdg  10182  frecuzrdgrcl  10183  frecuzrdgsuc  10187  frecuzrdgrclt  10188  frecuzrdgsuctlem  10196  fisumcom2  11207  sqpweven  11853  2sqpwodd  11854  phimullem  11901  txuni2  12425  txcnp  12440  txcnmpt  12442  txdis1cn  12447  txlm  12448  xmeterval  12604  limccnp2lem  12814  limccnp2cntop  12815