Theorem opelxpi 4808

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 4806	. 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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   <.cop 3712   X. cxp 4774

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-opab 4194  df-xp 4782

This theorem is used by:  opelxpd  4809  opelvvg  4826  opelvv  4827  opbrop  4856  fnbrfvb2  5748  fliftrel  6001  fnotovb  6134  ovi3  6229  ovres  6232  fovcdm  6235  fnovrn  6240  ovconst2  6244  oprab2co  6458  1stconst  6461  2ndconst  6462  f1od2  6475  brdifun  6839  ecopqsi  6869  brecop  6904  th3q  6919  xpcomco  7130  xpf1o  7150  xpmapenlem  7155  djulclr  7395  djurclr  7396  djulcl  7397  djurcl  7398  djuf1olem  7399  cc2lem  7638  addpiord  7689  mulpiord  7690  enqeceq  7732  1nq  7739  addpipqqslem  7742  mulpipq  7745  mulpipqqs  7746  addclnq  7748  mulclnq  7749  recexnq  7763  ltexnqq  7781  prarloclemarch  7791  prarloclemarch2  7792  nnnq  7795  enq0breq  7809  enq0eceq  7810  nqnq0  7814  addnnnq0  7822  mulnnnq0  7823  addclnq0  7824  mulclnq0  7825  nqpnq0nq  7826  prarloclemlt  7866  prarloclemlo  7867  prarloclemcalc  7875  genpelxp  7884  nqprm  7915  ltexprlempr  7981  recexprlempr  8005  cauappcvgprlemcl  8026  cauappcvgprlemladd  8031  caucvgprlemcl  8049  caucvgprprlemcl  8077  enreceq  8109  addsrpr  8118  mulsrpr  8119  0r  8123  1sr  8124  m1r  8125  addclsr  8126  mulclsr  8127  prsrcl  8157  mappsrprg  8177  addcnsr  8207  mulcnsr  8208  addcnsrec  8215  mulcnsrec  8216  pitonnlem2  8220  pitonn  8221  pitore  8223  recnnre  8224  axaddcl  8237  axmulcl  8239  xrlenlt  8396  frecuzrdgg  10873  frecuzrdgsuctlem  10880  seq3val  10917  swrdval  11441  cnrecnv  11697  eucalgf  12857  eucalg  12861  qredeu  12899  qnumdenbi  12996  crth  13030  phimullem  13031  setscom  13449  setsslid  13460  imasaddfnlemg  13693  imasaddflemg  13695  txbas  15501  upxp  15515  uptx  15517  txlm  15522  cnmpt21  15534  txswaphmeolem  15563  txswaphmeo  15564  comet  15742  qtopbasss  15764  cnmetdval  15772  remetdval  15790  tgqioo  15798  dvcnp2cntop  15942  dvef  15970  djucllem  17050  pwle2  17250