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  6838  ecopqsi  6868  brecop  6903  th3q  6918  xpcomco  7128  xpf1o  7148  xpmapenlem  7153  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  10874  frecuzrdgsuctlem  10881  seq3val  10918  swrdval  11442  cnrecnv  11698  eucalgf  12858  eucalg  12862  qredeu  12900  qnumdenbi  12997  crth  13031  phimullem  13032  setscom  13450  setsslid  13461  imasaddfnlemg  13694  imasaddflemg  13696  txbas  15484  upxp  15498  uptx  15500  txlm  15505  cnmpt21  15517  txswaphmeolem  15546  txswaphmeo  15547  comet  15725  qtopbasss  15747  cnmetdval  15755  remetdval  15773  tgqioo  15781  dvcnp2cntop  15925  dvef  15953  djucllem  17033  pwle2  17233