Theorem opelxp 4967

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 4956	. 2 |- ( <. A , B >. e. ( C X. D ) <-> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
2		vex 3071	. . . . . . 7 |- x e. _V
3		vex 3071	. . . . . . 7 |- y e. _V
4	2, 3	opth2 4668	. . . . . 6 |- ( <. A , B >. = <. x , y >. <-> ( A = x /\ B = y ) )
5		eleq1 2523	. . . . . . 7 |- ( A = x -> ( A e. C <-> x e. C ) )
6		eleq1 2523	. . . . . . 7 |- ( B = y -> ( B e. D <-> y e. D ) )
7	5, 6	bi2anan9 868	. . . . . 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 2942	. . 3 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) )
11		eqid 2451	. . . 4 |- <. A , B >. = <. A , B >.
12		opeq1 4157	. . . . . 6 |- ( x = A -> <. x , y >. = <. A , y >. )
13	12	eqeq2d 2465	. . . . 5 |- ( x = A -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. A , y >. ) )
14		opeq2 4158	. . . . . 6 |- ( y = B -> <. A , y >. = <. A , B >. )
15	14	eqeq2d 2465	. . . . 5 |- ( y = B -> ( <. A , B >. = <. A , y >. <-> <. A , B >. = <. A , B >. ) )
16	13, 15	rspc2ev 3178	. . . 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 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 1370   e. wcel 1758   E.wrex 2796   <.cop 3981   X. cxp 4936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pr 4629

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-opab 4449  df-xp 4944

This theorem is referenced by:  brxp  4968  opelxpi  4969  opelxp1  4970  opelxp2  4971  opthprc  4984  elxp3  4987  opeliunxp  4988  optocl  5011  xpsspwOLD  5052  xpiindi  5073  opelres  5214  restidsing  5260  codir  5316  qfto  5317  xpnz  5355  difxp  5360  xpdifid  5364  ssrnres  5374  dfco2  5435  relssdmrn  5456  ressn  5471  opelf  5672  oprab4  6256  resoprab  6286  oprssdm  6344  nssdmovg  6345  ndmovg  6346  elmpt2cl  6404  resiexg  6614  fo1stres  6700  fo2ndres  6701  dfoprab4  6731  opiota  6733  bropopvvv  6753  curry1  6764  curry2  6767  xporderlem  6783  fnwelem  6787  mpt2xopxprcov0  6834  mpt2curryd  6888  brecop  7293  brecop2  7294  eceqoveq  7305  xpdom2  7506  mapunen  7580  dfac5lem2  8395  iunfo  8804  ordpipq  9212  opelcn  9397  opelreal  9398  elreal2  9400  swrd00  12416  swrdcl  12417  swrd0  12429  fsumcom2  13343  phimullem  13956  imasvscafn  14577  homarcl2  15005  evlfcl  15134  clatl  15388  mdetrlin  18524  iscnp2  18959  txuni2  19254  txcls  19293  txcnpi  19297  txcnp  19309  txcnmpt  19313  txdis1cn  19324  txtube  19329  hausdiag  19334  txlm  19337  tx1stc  19339  txkgen  19341  txflf  19695  tmdcn2  19776  tgphaus  19803  divstgplem  19807  fmucndlem  19982  xmeterval  20123  metustexhalfOLD  20254  metustexhalf  20255  blval2  20266  metuel2  20270  bcthlem1  20951  ovolfcl  21066  ovoliunlem1  21101  ovolshftlem1  21108  mbfimaopnlem  21249  limccnp2  21483  cxpcn3  22302  fsumvma  22668  lgsquadlem1  22809  lgsquadlem2  22810  ofresid  26094  xppreima2  26099  f1od2  26158  eulerpartlemgvv  26893  erdszelem10  27222  cvmlift2lem10  27335  cvmlift2lem12  27337  fprodcom2  27629  dfso2  27698  txpss3v  28043  pprodss4v  28049  dfrdg4  28115  heiborlem3  28850  pellex  29314  ndmaovg  30228  aoprssdm  30246  ndmaovcl  30247  ndmaovrcl  30248  ndmaovcom  30249  ndmaovass  30250  ndmaovdistr  30251  el2xptp0  30265  otel3xp  30266  2wlkonot3v  30532  2spthonot3v  30533  2wlkonotv  30534  numclwlk1lem2f  30823  opeliun2xp  30858  matplusgcell  31005  dibopelvalN  35094  dibopelval2  35096  dib1dim  35116  dihopcl  35204  dih1  35237  dih1dimatlem  35280  hdmap1val  35750