Theorem opelxp 5146

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 5132	. 2 |- ( <. A , B >. e. ( C X. D ) <-> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
2		vex 3203	. . . . . . 7 |- x e. _V
3		vex 3203	. . . . . . 7 |- y e. _V
4	2, 3	opth2 4949	. . . . . 6 |- ( <. A , B >. = <. x , y >. <-> ( A = x /\ B = y ) )
5		eleq1 2689	. . . . . . 7 |- ( A = x -> ( A e. C <-> x e. C ) )
6		eleq1 2689	. . . . . . 7 |- ( B = y -> ( B e. D <-> y e. D ) )
7	5, 6	bi2anan9 917	. . . . . 6 |- ( ( A = x /\ B = y ) -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
8	4, 7	sylbi 207	. . . . 5 |- ( <. A , B >. = <. x , y >. -> ( ( A e. C /\ B e. D ) <-> ( x e. C /\ y e. D ) ) )
9	8	biimprcd 240	. . . 4 |- ( ( x e. C /\ y e. D ) -> ( <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) ) )
10	9	rexlimivv 3036	. . 3 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. -> ( A e. C /\ B e. D ) )
11		eqid 2622	. . . 4 |- <. A , B >. = <. A , B >.
12		opeq1 4402	. . . . . 6 |- ( x = A -> <. x , y >. = <. A , y >. )
13	12	eqeq2d 2632	. . . . 5 |- ( x = A -> ( <. A , B >. = <. x , y >. <-> <. A , B >. = <. A , y >. ) )
14		opeq2 4403	. . . . . 6 |- ( y = B -> <. A , y >. = <. A , B >. )
15	14	eqeq2d 2632	. . . . 5 |- ( y = B -> ( <. A , B >. = <. A , y >. <-> <. A , B >. = <. A , B >. ) )
16	13, 15	rspc2ev 3324	. . . 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 1413	. . 3 |- ( ( A e. C /\ B e. D ) -> E. x e. C E. y e. D <. A , B >. = <. x , y >. )
18	10, 17	impbii 199	. 2 |- ( E. x e. C E. y e. D <. A , B >. = <. x , y >. <-> ( A e. C /\ B e. D ) )
19	1, 18	bitri 264	1 |- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )

Syntax hints:   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   E.wrex 2913   <.cop 4183   X. cxp 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-opab 4713  df-xp 5120

This theorem is referenced by:  brxp  5147  opelxpi  5148  opelxp1  5150  opelxp2  5151  otel3xp  5153  opthprc  5167  elxp3  5169  opeliunxp  5170  bropaex12  5192  optocl  5195  xpsspw  5233  xpiindi  5257  opelres  5401  restidsing  5458  restidsingOLD  5459  codir  5516  qfto  5517  xpnz  5553  difxp  5558  xpdifid  5562  ssrnres  5572  dfco2  5634  relssdmrn  5656  ressn  5671  elsnxpOLD  5678  opelf  6065  oprab4  6726  resoprab  6756  oprssdm  6815  nssdmovg  6816  ndmovg  6817  elmpt2cl  6876  resiexg  7102  fo1stres  7192  fo2ndres  7193  el2xptp0  7212  dfoprab4  7225  opiota  7229  bropopvvv  7255  bropfvvvvlem  7256  curry1  7269  curry2  7272  xporderlem  7288  fnwelem  7292  mpt2xopxprcov0  7343  mpt2curryd  7395  brecop  7840  brecop2  7841  eceqoveq  7853  xpdom2  8055  mapunen  8129  dfac5lem2  8947  iunfo  9361  ordpipq  9764  prsrlem1  9893  opelcn  9950  opelreal  9951  elreal2  9953  swrd00  13418  swrdcl  13419  swrd0  13434  fsumcom2  14505  fsumcom2OLD  14506  fprodcom2  14714  fprodcom2OLD  14715  phimullem  15484  imasvscafn  16197  brcic  16458  homarcl2  16685  evlfcl  16862  clatl  17116  matplusgcell  20239  mdetrlin  20408  iscnp2  21043  txuni2  21368  txcls  21407  txcnpi  21411  txcnp  21423  txcnmpt  21427  txdis1cn  21438  txtube  21443  hausdiag  21448  txlm  21451  tx1stc  21453  txkgen  21455  txflf  21810  tmdcn2  21893  tgphaus  21920  qustgplem  21924  fmucndlem  22095  xmeterval  22237  metustexhalf  22361  blval2  22367  metuel2  22370  bcthlem1  23121  ovolfcl  23235  ovoliunlem1  23270  ovolshftlem1  23277  mbfimaopnlem  23422  limccnp2  23656  cxpcn3  24489  fsumvma  24938  lgsquadlem1  25105  lgsquadlem2  25106  ofresid  29444  xppreima2  29450  aciunf1lem  29462  f1od2  29499  smatrcl  29862  smatlem  29863  qtophaus  29903  eulerpartlemgvv  30438  erdszelem10  31182  cvmlift2lem10  31294  cvmlift2lem12  31296  msubff  31427  elmpst  31433  mpstrcl  31438  elmpps  31470  dfso2  31644  fv1stcnv  31680  fv2ndcnv  31681  txpss3v  31985  pprodss4v  31991  dfrdg4  32058  bj-elid3  33087  bj-eldiag2  33092  curf  33387  curunc  33391  heiborlem3  33612  opelresALTV  34031  xrnss3v  34135  dibopelvalN  36432  dibopelval2  36434  dib1dim  36454  dihopcl  36542  dih1  36575  dih1dimatlem  36618  hdmap1val  37088  pellex  37399  elnonrel  37891  fourierdlem42  40366  etransclem44  40495  ovn0lem  40779  ndmaovg  41264  aoprssdm  41282  ndmaovcl  41283  ndmaovrcl  41284  ndmaovcom  41285  ndmaovass  41286  ndmaovdistr  41287  pfx00  41384  pfx0  41385  sprsymrelfvlem  41740  sprsymrelfolem2  41743  opeliun2xp  42111