Theorem opelxpi 4708

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 4706	. 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 2176   <.cop 3636   X. cxp 4674

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4163  ax-pow 4219  ax-pr 4254

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-opab 4107  df-xp 4682

This theorem is referenced by:  opelxpd  4709  opelvvg  4725  opelvv  4726  opbrop  4755  fliftrel  5863  fnotovb  5990  ovi3  6085  ovres  6088  fovcdm  6091  fnovrn  6096  ovconst2  6100  oprab2co  6306  1stconst  6309  2ndconst  6310  f1od2  6323  brdifun  6649  ecopqsi  6679  brecop  6714  th3q  6729  xpcomco  6923  xpf1o  6943  xpmapenlem  6948  djulclr  7153  djurclr  7154  djulcl  7155  djurcl  7156  djuf1olem  7157  cc2lem  7380  addpiord  7431  mulpiord  7432  enqeceq  7474  1nq  7481  addpipqqslem  7484  mulpipq  7487  mulpipqqs  7488  addclnq  7490  mulclnq  7491  recexnq  7505  ltexnqq  7523  prarloclemarch  7533  prarloclemarch2  7534  nnnq  7537  enq0breq  7551  enq0eceq  7552  nqnq0  7556  addnnnq0  7564  mulnnnq0  7565  addclnq0  7566  mulclnq0  7567  nqpnq0nq  7568  prarloclemlt  7608  prarloclemlo  7609  prarloclemcalc  7617  genpelxp  7626  nqprm  7657  ltexprlempr  7723  recexprlempr  7747  cauappcvgprlemcl  7768  cauappcvgprlemladd  7773  caucvgprlemcl  7791  caucvgprprlemcl  7819  enreceq  7851  addsrpr  7860  mulsrpr  7861  0r  7865  1sr  7866  m1r  7867  addclsr  7868  mulclsr  7869  prsrcl  7899  mappsrprg  7919  addcnsr  7949  mulcnsr  7950  addcnsrec  7957  mulcnsrec  7958  pitonnlem2  7962  pitonn  7963  pitore  7965  recnnre  7966  axaddcl  7979  axmulcl  7981  xrlenlt  8139  frecuzrdgg  10563  frecuzrdgsuctlem  10570  seq3val  10607  swrdval  11104  cnrecnv  11254  eucalgf  12410  eucalg  12414  qredeu  12452  qnumdenbi  12547  crth  12579  phimullem  12580  setscom  12905  setsslid  12916  imasaddfnlemg  13179  imasaddflemg  13181  txbas  14763  upxp  14777  uptx  14779  txlm  14784  cnmpt21  14796  txswaphmeolem  14825  txswaphmeo  14826  comet  15004  qtopbasss  15026  cnmetdval  15034  remetdval  15052  tgqioo  15060  dvcnp2cntop  15204  dvef  15232  djucllem  15773  pwle2  15972