Theorem opelxpi 4660

Description: Ordered pair membership in a cross product (implication). (Contributed by NM, 28-May-1995.)

Assertion

Ref	Expression
opelxpi	|- ( ( A e. C /\ B e. D ) -> <. A , B >. e. ( C X. D ) )

Proof of Theorem opelxpi

Step	Hyp	Ref	Expression
1		opelxp 4658	. 2 |- ( <. A , B >. e. ( C X. D ) <-> ( A e. C /\ B e. D ) )
2	1	biimpri 133	1 |- ( ( A e. C /\ B e. D ) -> <. A , B >. e. ( C X. D ) )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2148   <.cop 3597   X. cxp 4626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-pr 4211

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2741  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-opab 4067  df-xp 4634

This theorem is referenced by:  opelxpd  4661  opelvvg  4677  opelvv  4678  opbrop  4707  fliftrel  5795  fnotovb  5920  ovi3  6013  ovres  6016  fovcdm  6019  fnovrn  6024  ovconst2  6028  oprab2co  6221  1stconst  6224  2ndconst  6225  f1od2  6238  brdifun  6564  ecopqsi  6592  brecop  6627  th3q  6642  xpcomco  6828  xpf1o  6846  xpmapenlem  6851  djulclr  7050  djurclr  7051  djulcl  7052  djurcl  7053  djuf1olem  7054  cc2lem  7267  addpiord  7317  mulpiord  7318  enqeceq  7360  1nq  7367  addpipqqslem  7370  mulpipq  7373  mulpipqqs  7374  addclnq  7376  mulclnq  7377  recexnq  7391  ltexnqq  7409  prarloclemarch  7419  prarloclemarch2  7420  nnnq  7423  enq0breq  7437  enq0eceq  7438  nqnq0  7442  addnnnq0  7450  mulnnnq0  7451  addclnq0  7452  mulclnq0  7453  nqpnq0nq  7454  prarloclemlt  7494  prarloclemlo  7495  prarloclemcalc  7503  genpelxp  7512  nqprm  7543  ltexprlempr  7609  recexprlempr  7633  cauappcvgprlemcl  7654  cauappcvgprlemladd  7659  caucvgprlemcl  7677  caucvgprprlemcl  7705  enreceq  7737  addsrpr  7746  mulsrpr  7747  0r  7751  1sr  7752  m1r  7753  addclsr  7754  mulclsr  7755  prsrcl  7785  mappsrprg  7805  addcnsr  7835  mulcnsr  7836  addcnsrec  7843  mulcnsrec  7844  pitonnlem2  7848  pitonn  7849  pitore  7851  recnnre  7852  axaddcl  7865  axmulcl  7867  xrlenlt  8024  frecuzrdgg  10418  frecuzrdgsuctlem  10425  seq3val  10460  cnrecnv  10921  eucalgf  12057  eucalg  12061  qredeu  12099  qnumdenbi  12194  crth  12226  phimullem  12227  setscom  12504  setsslid  12515  imasaddfnlemg  12740  imasaddflemg  12742  txbas  13797  upxp  13811  uptx  13813  txlm  13818  cnmpt21  13830  txswaphmeolem  13859  txswaphmeo  13860  comet  14038  qtopbasss  14060  cnmetdval  14068  remetdval  14078  tgqioo  14086  dvcnp2cntop  14202  dvef  14227  djucllem  14591  pwle2  14787