Theorem opelxp 4882

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 4870	. 2 |- ( <. A , B >. e. ( C X. D ) <-> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
2		vex 3059	. . . . . . 7 |- x e. _V
3		vex 3059	. . . . . . 7 |- y e. _V
4	2, 3	opth2 4693	. . . . . 6 |- ( <. A , B >. = <. x , y >. <-> ( A = x /\ B = y ) )
5		eleq1 2527	. . . . . . 7 |- ( A = x -> ( A e. C <-> x e. C ) )
6		eleq1 2527	. . . . . . 7 |- ( B = y -> ( B e. D <-> y e. D ) )
7	5, 6	bi2anan9 889	. . . . . 6 |- ( ( A = x /\ B = y ) -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
8	4, 7	sylbi 200	. . . . 5 |- ( <. A , B >. = <. x , y >. -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
9	8	biimprcd 233	. . . 4 |- ( ( x e. C /\ y e. D ) -> ( <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) ) )
10	9	rexlimivv 2895	. . 3 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) )
11		eqid 2461	. . . 4 |- <. A , B >. = <. A , B >.
12		opeq1 4179	. . . . . 6 |- ( x = A -> <. x , y >. = <. A , y >. )
13	12	eqeq2d 2471	. . . . 5 |- ( x = A -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. A , y >. ) )
14		opeq2 4180	. . . . . 6 |- ( y = B -> <. A , y >. = <. A , B >. )
15	14	eqeq2d 2471	. . . . 5 |- ( y = B -> ( <. A , B >. = <. A , y >. <-> <. A , B >. = <. A , B >. ) )
16	13, 15	rspc2ev 3172	. . . 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 1362	. . 3 |- ( ( A e. C /\ B e. D ) -> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
18	10, 17	impbii 192	. 2 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. <-> ( A e. C /\ B e. D ) )
19	1, 18	bitri 257	1 |- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )

Syntax hints:   <-> wb 189   /\ wa 375   = wceq 1454   e. wcel 1897   E.wrex 2749   <.cop 3985   X. cxp 4850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pr 4652

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-opab 4475  df-xp 4858

This theorem is referenced by:  brxp  4883  opelxpi  4884  opelxp1  4885  opelxp2  4886  otel3xp  4888  opthprc  4900  elxp3  4903  opeliunxp  4904  bropaex12  4926  optocl  4929  xpsspw  4966  xpiindi  4988  opelres  5128  restidsing  5179  codir  5238  qfto  5239  xpnz  5274  difxp  5279  xpdifid  5283  ssrnres  5293  dfco2  5352  relssdmrn  5374  ressn  5390  elsnxp  5396  opelf  5767  oprab4  6388  resoprab  6418  oprssdm  6476  nssdmovg  6477  ndmovg  6478  elmpt2cl  6537  resiexg  6755  fo1stres  6843  fo2ndres  6844  el2xptp0  6863  dfoprab4  6876  opiota  6878  bropopvvv  6900  bropfvvvvlem  6901  curry1  6914  curry2  6917  xporderlem  6933  fnwelem  6937  mpt2xopxprcov0  6989  mpt2curryd  7041  brecop  7481  brecop2  7482  eceqoveq  7493  xpdom2  7692  mapunen  7766  dfac5lem2  8580  iunfo  8989  ordpipq  9392  prsrlem1  9521  opelcn  9578  opelreal  9579  elreal2  9581  swrd00  12810  swrdcl  12811  swrd0  12826  fsumcom2  13883  fprodcom2  14086  phimullem  14775  imasvscafn  15491  brcic  15751  homarcl2  15978  evlfcl  16155  clatl  16410  matplusgcell  19506  mdetrlin  19675  iscnp2  20303  txuni2  20628  txcls  20667  txcnpi  20671  txcnp  20683  txcnmpt  20687  txdis1cn  20698  txtube  20703  hausdiag  20708  txlm  20711  tx1stc  20713  txkgen  20715  txflf  21069  tmdcn2  21152  tgphaus  21179  qustgplem  21183  fmucndlem  21354  xmeterval  21495  metustexhalf  21619  blval2  21625  metuel2  21628  bcthlem1  22340  ovolfcl  22467  ovoliunlem1  22503  ovolshftlem1  22510  mbfimaopnlem  22659  limccnp2  22895  cxpcn3  23736  fsumvma  24189  lgsquadlem1  24330  lgsquadlem2  24331  2wlkonot3v  25651  2spthonot3v  25652  2wlkonotv  25653  numclwlk1lem2f  25868  ofresid  28291  xppreima2  28297  aciunf1lem  28312  f1od2  28357  smatrcl  28670  smatlem  28671  qtophaus  28711  esum2dlem  28961  eulerpartlemgvv  29257  erdszelem10  29971  cvmlift2lem10  30083  cvmlift2lem12  30085  msubff  30216  elmpst  30222  mpstrcl  30227  elmpps  30259  dfso2  30442  fv1stcnv  30470  fv2ndcnv  30471  txpss3v  30693  pprodss4v  30699  dfrdg4  30766  bj-elid3  31686  bj-eldiag2  31691  heiborlem3  32189  dibopelvalN  34755  dibopelval2  34757  dib1dim  34777  dihopcl  34865  dih1  34898  dih1dimatlem  34941  hdmap1val  35411  pellex  35723  elnonrel  36235  fourierdlem42  38049  fourierdlem42OLD  38050  etransclem44  38180  ovn0lem  38424  ndmaovg  38723  aoprssdm  38741  ndmaovcl  38742  ndmaovrcl  38743  ndmaovcom  38744  ndmaovass  38745  ndmaovdistr  38746  pfx00  38964  pfx0  38965  opeliun2xp  40386