Theorem opelxp 4826

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 4814	. 2 |- ( <. A , B >. e. ( C X. D ) <-> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
2		vex 3025	. . . . . . 7 |- x e. _V
3		vex 3025	. . . . . . 7 |- y e. _V
4	2, 3	opth2 4642	. . . . . 6 |- ( <. A , B >. = <. x , y >. <-> ( A = x /\ B = y ) )
5		eleq1 2494	. . . . . . 7 |- ( A = x -> ( A e. C <-> x e. C ) )
6		eleq1 2494	. . . . . . 7 |- ( B = y -> ( B e. D <-> y e. D ) )
7	5, 6	bi2anan9 881	. . . . . 6 |- ( ( A = x /\ B = y ) -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
8	4, 7	sylbi 198	. . . . 5 |- ( <. A , B >. = <. x , y >. -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
9	8	biimprcd 228	. . . 4 |- ( ( x e. C /\ y e. D ) -> ( <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) ) )
10	9	rexlimivv 2861	. . 3 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) )
11		eqid 2428	. . . 4 |- <. A , B >. = <. A , B >.
12		opeq1 4130	. . . . . 6 |- ( x = A -> <. x , y >. = <. A , y >. )
13	12	eqeq2d 2438	. . . . 5 |- ( x = A -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. A , y >. ) )
14		opeq2 4131	. . . . . 6 |- ( y = B -> <. A , y >. = <. A , B >. )
15	14	eqeq2d 2438	. . . . 5 |- ( y = B -> ( <. A , B >. = <. A , y >. <-> <. A , B >. = <. A , B >. ) )
16	13, 15	rspc2ev 3136	. . . 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 1349	. . 3 |- ( ( A e. C /\ B e. D ) -> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
18	10, 17	impbii 190	. 2 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. <-> ( A e. C /\ B e. D ) )
19	1, 18	bitri 252	1 |- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )

Syntax hints:   <-> wb 187   /\ wa 370   = wceq 1437   e. wcel 1872   E.wrex 2715   <.cop 3947   X. cxp 4794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pr 4603

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-opab 4426  df-xp 4802

This theorem is referenced by:  brxp  4827  opelxpi  4828  opelxp1  4829  opelxp2  4830  otel3xp  4832  opthprc  4844  elxp3  4847  opeliunxp  4848  bropaex12  4870  optocl  4873  xpsspw  4910  xpiindi  4932  opelres  5072  restidsing  5123  codir  5182  qfto  5183  xpnz  5218  difxp  5223  xpdifid  5227  ssrnres  5237  dfco2  5296  relssdmrn  5318  ressn  5334  elsnxp  5340  opelf  5705  oprab4  6320  resoprab  6350  oprssdm  6408  nssdmovg  6409  ndmovg  6410  elmpt2cl  6469  resiexg  6687  fo1stres  6775  fo2ndres  6776  el2xptp0  6795  dfoprab4  6808  opiota  6810  bropopvvv  6831  curry1  6843  curry2  6846  xporderlem  6862  fnwelem  6866  mpt2xopxprcov0  6918  mpt2curryd  6971  brecop  7411  brecop2  7412  eceqoveq  7423  xpdom2  7620  mapunen  7694  dfac5lem2  8506  iunfo  8915  ordpipq  9318  prsrlem1  9447  opelcn  9504  opelreal  9505  elreal2  9507  swrd00  12720  swrdcl  12721  swrd0  12736  fsumcom2  13778  fprodcom2  13981  phimullem  14670  imasvscafn  15386  brcic  15646  homarcl2  15873  evlfcl  16050  clatl  16305  matplusgcell  19400  mdetrlin  19569  iscnp2  20197  txuni2  20522  txcls  20561  txcnpi  20565  txcnp  20577  txcnmpt  20581  txdis1cn  20592  txtube  20597  hausdiag  20602  txlm  20605  tx1stc  20607  txkgen  20609  txflf  20963  tmdcn2  21046  tgphaus  21073  qustgplem  21077  fmucndlem  21248  xmeterval  21389  metustexhalf  21513  blval2  21519  metuel2  21522  bcthlem1  22234  ovolfcl  22361  ovoliunlem1  22397  ovolshftlem1  22404  mbfimaopnlem  22553  limccnp2  22789  cxpcn3  23630  fsumvma  24083  lgsquadlem1  24224  lgsquadlem2  24225  2wlkonot3v  25545  2spthonot3v  25546  2wlkonotv  25547  numclwlk1lem2f  25762  ofresid  28189  xppreima2  28195  aciunf1lem  28210  f1od2  28259  smatrcl  28574  smatlem  28575  qtophaus  28615  esum2dlem  28865  eulerpartlemgvv  29161  erdszelem10  29875  cvmlift2lem10  29987  cvmlift2lem12  29989  msubff  30120  elmpst  30126  mpstrcl  30131  elmpps  30163  dfso2  30345  fv1stcnv  30373  fv2ndcnv  30374  txpss3v  30594  pprodss4v  30600  dfrdg4  30667  bj-elid3  31548  bj-eldiag2  31554  heiborlem3  32052  dibopelvalN  34623  dibopelval2  34625  dib1dim  34645  dihopcl  34733  dih1  34766  dih1dimatlem  34809  hdmap1val  35279  pellex  35592  elnonrel  36104  fourierdlem42  37895  fourierdlem42OLD  37896  etransclem44  38026  ovn0lem  38234  ndmaovg  38499  aoprssdm  38517  ndmaovcl  38518  ndmaovrcl  38519  ndmaovcom  38520  ndmaovass  38521  ndmaovdistr  38522  pfx00  38738  pfx0  38739  opeliun2xp  39717