Theorem opelxp 4761

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 4749	. 2 |- ( <. A , B >. e. ( C X. D ) <-> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
2		vex 2806	. . . . . . 7 |- x e. _V
3		vex 2806	. . . . . . 7 |- y e. _V
4	2, 3	opth2 4338	. . . . . 6 |- ( <. A , B >. = <. x , y >. <-> ( A = x /\ B = y ) )
5		eleq1 2294	. . . . . . 7 |- ( A = x -> ( A e. C <-> x e. C ) )
6		eleq1 2294	. . . . . . 7 |- ( B = y -> ( B e. D <-> y e. D ) )
7	5, 6	bi2anan9 610	. . . . . 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 2657	. . 3 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) )
11		eqid 2231	. . . 4 |- <. A , B >. = <. A , B >.
12		opeq1 3867	. . . . . 6 |- ( x = A -> <. x , y >. = <. A , y >. )
13	12	eqeq2d 2243	. . . . 5 |- ( x = A -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. A , y >. ) )
14		opeq2 3868	. . . . . 6 |- ( y = B -> <. A , y >. = <. A , B >. )
15	14	eqeq2d 2243	. . . . 5 |- ( y = B -> ( <. A , B >. = <. A , y >. <-> <. A , B >. = <. A , B >. ) )
16	13, 15	rspc2ev 2926	. . . 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 1363	. . 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 1398   e. wcel 2202   E.wrex 2512   <.cop 3676   X. cxp 4729

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-v 2805  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-opab 4156  df-xp 4737

This theorem is referenced by:  brxp  4762  opelxpi  4763  opelxp1  4765  opelxp2  4766  opthprc  4783  elxp3  4786  opeliunxp  4787  optocl  4808  xpiindim  4873  opelres  5024  resiexg  5064  restidsing  5075  codir  5132  qfto  5133  xpmlem  5164  rnxpid  5178  ssrnres  5186  dfco2  5243  relssdmrn  5264  ressn  5284  opelf  5515  fnovex  6061  oprab4  6102  resoprab  6127  elmpocl  6227  fo1stresm  6333  fo2ndresm  6334  dfoprab4  6364  xporderlem  6405  f1od2  6409  brecop  6837  xpdom2  7058  djulclb  7314  djuss  7329  enq0enq  7711  enq0sym  7712  enq0tr  7714  nqnq0pi  7718  nnnq0lem1  7726  elinp  7754  genipv  7789  prsrlem1  8022  gt0srpr  8028  opelcn  8106  opelreal  8107  elreal2  8110  frecuzrdgrrn  10733  frec2uzrdg  10734  frecuzrdgrcl  10735  frecuzrdgsuc  10739  frecuzrdgrclt  10740  frecuzrdgsuctlem  10748  fisumcom2  12079  fprodcom2fi  12267  sqpweven  12827  2sqpwodd  12828  phimullem  12877  relelbasov  13225  txuni2  15067  txcnp  15082  txcnmpt  15084  txdis1cn  15089  txlm  15090  xmeterval  15246  limccnp2lem  15487  limccnp2cntop  15488  lgsquadlem1  15896  lgsquadlem2  15897