Theorem opelxp 4856

Description: Ordered pair membership in a Cartesian 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 4845	. 2 |- ( <. A , B >. e. ( C X. D ) <-> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
2		vex 2965	. . . . . . 7 |- x e. _V
3		vex 2965	. . . . . . 7 |- y e. _V
4	2, 3	opth2 4558	. . . . . 6 |- ( <. A , B >. = <. x , y >. <-> ( A = x /\ B = y ) )
5		eleq1 2493	. . . . . . 7 |- ( A = x -> ( A e. C <-> x e. C ) )
6		eleq1 2493	. . . . . . 7 |- ( B = y -> ( B e. D <-> y e. D ) )
7	5, 6	bi2anan9 861	. . . . . 6 |- ( ( A = x /\ B = y ) -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
8	4, 7	sylbi 195	. . . . 5 |- ( <. A , B >. = <. x , y >. -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
9	8	biimprcd 225	. . . 4 |- ( ( x e. C /\ y e. D ) -> ( <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) ) )
10	9	rexlimivv 2836	. . 3 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) )
11		eqid 2433	. . . 4 |- <. A , B >. = <. A , B >.
12		opeq1 4047	. . . . . 6 |- ( x = A -> <. x , y >. = <. A , y >. )
13	12	eqeq2d 2444	. . . . 5 |- ( x = A -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. A , y >. ) )
14		opeq2 4048	. . . . . 6 |- ( y = B -> <. A , y >. = <. A , B >. )
15	14	eqeq2d 2444	. . . . 5 |- ( y = B -> ( <. A , B >. = <. A , y >. <-> <. A , B >. = <. A , B >. ) )
16	13, 15	rspc2ev 3070	. . . 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 1296	. . 3 |- ( ( A e. C /\ B e. D ) -> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
18	10, 17	impbii 188	. 2 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. <-> ( A e. C /\ B e. D ) )
19	1, 18	bitri 249	1 |- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )

Syntax hints:   <-> wb 184   /\ wa 369   = wceq 1362   e. wcel 1755   E.wrex 2706   <.cop 3871   X. cxp 4825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-opab 4339  df-xp 4833

This theorem is referenced by:  brxp  4857  opelxpi  4858  opelxp1  4859  opelxp2  4860  opthprc  4873  elxp3  4876  opeliunxp  4877  optocl  4900  xpsspwOLD  4941  xpiindi  4962  opelres  5103  restidsing  5150  codir  5206  qfto  5207  xpnz  5245  difxp  5250  xpdifid  5254  ssrnres  5264  dfco2  5325  relssdmrn  5346  ressn  5361  opelf  5562  oprab4  6146  resoprab  6175  oprssdm  6233  nssdmovg  6234  ndmovg  6235  elmpt2cl  6293  resiexg  6503  fo1stres  6589  fo2ndres  6590  dfoprab4  6620  opiota  6622  bropopvvv  6642  curry1  6653  curry2  6656  xporderlem  6672  fnwelem  6676  mpt2xopxprcov0  6723  brecop  7181  brecop2  7182  eceqoveq  7193  xpdom2  7394  mapunen  7468  dfac5lem2  8282  iunfo  8691  ordpipq  9099  opelcn  9284  opelreal  9285  elreal2  9287  swrd00  12298  swrdcl  12299  swrd0  12311  fsumcom2  13225  phimullem  13837  imasvscafn  14458  homarcl2  14886  evlfcl  15015  clatl  15269  mdetrlin  18251  iscnp2  18685  txuni2  18980  txcls  19019  txcnpi  19023  txcnp  19035  txcnmpt  19039  txdis1cn  19050  txtube  19055  hausdiag  19060  txlm  19063  tx1stc  19065  txkgen  19067  txflf  19421  tmdcn2  19502  tgphaus  19529  divstgplem  19533  fmucndlem  19708  xmeterval  19849  metustexhalfOLD  19980  metustexhalf  19981  blval2  19992  metuel2  19996  bcthlem1  20677  ovolfcl  20792  ovoliunlem1  20827  ovolshftlem1  20834  mbfimaopnlem  20975  limccnp2  21209  cxpcn3  22071  fsumvma  22437  lgsquadlem1  22578  lgsquadlem2  22579  ofresid  25784  xppreima2  25789  f1od2  25848  eulerpartlemgvv  26607  erdszelem10  26936  cvmlift2lem10  27049  cvmlift2lem12  27051  fprodcom2  27342  dfso2  27411  txpss3v  27756  pprodss4v  27762  dfrdg4  27828  heiborlem3  28556  pellex  29021  ndmaovg  29936  aoprssdm  29954  ndmaovcl  29955  ndmaovrcl  29956  ndmaovcom  29957  ndmaovass  29958  ndmaovdistr  29959  el2xptp0  29973  otel3xp  29974  2wlkonot3v  30240  2spthonot3v  30241  2wlkonotv  30242  numclwlk1lem2f  30531  opeliun2xp  30565  matplusgcell  30640  dibopelvalN  34361  dibopelval2  34363  dib1dim  34383  dihopcl  34471  dih1  34504  dih1dimatlem  34547  hdmap1val  35017