Theorem opelxpi 4757

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 4755	. 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 2202   <.cop 3672   X. cxp 4723

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-opab 4151  df-xp 4731

This theorem is referenced by:  opelxpd  4758  opelvvg  4775  opelvv  4776  opbrop  4805  fnbrfvb2  5688  fliftrel  5932  fnotovb  6063  ovi3  6158  ovres  6161  fovcdm  6164  fnovrn  6169  ovconst2  6173  oprab2co  6382  1stconst  6385  2ndconst  6386  f1od2  6399  brdifun  6728  ecopqsi  6758  brecop  6793  th3q  6808  xpcomco  7009  xpf1o  7029  xpmapenlem  7034  djulclr  7247  djurclr  7248  djulcl  7249  djurcl  7250  djuf1olem  7251  cc2lem  7484  addpiord  7535  mulpiord  7536  enqeceq  7578  1nq  7585  addpipqqslem  7588  mulpipq  7591  mulpipqqs  7592  addclnq  7594  mulclnq  7595  recexnq  7609  ltexnqq  7627  prarloclemarch  7637  prarloclemarch2  7638  nnnq  7641  enq0breq  7655  enq0eceq  7656  nqnq0  7660  addnnnq0  7668  mulnnnq0  7669  addclnq0  7670  mulclnq0  7671  nqpnq0nq  7672  prarloclemlt  7712  prarloclemlo  7713  prarloclemcalc  7721  genpelxp  7730  nqprm  7761  ltexprlempr  7827  recexprlempr  7851  cauappcvgprlemcl  7872  cauappcvgprlemladd  7877  caucvgprlemcl  7895  caucvgprprlemcl  7923  enreceq  7955  addsrpr  7964  mulsrpr  7965  0r  7969  1sr  7970  m1r  7971  addclsr  7972  mulclsr  7973  prsrcl  8003  mappsrprg  8023  addcnsr  8053  mulcnsr  8054  addcnsrec  8061  mulcnsrec  8062  pitonnlem2  8066  pitonn  8067  pitore  8069  recnnre  8070  axaddcl  8083  axmulcl  8085  xrlenlt  8243  frecuzrdgg  10677  frecuzrdgsuctlem  10684  seq3val  10721  swrdval  11228  cnrecnv  11470  eucalgf  12626  eucalg  12630  qredeu  12668  qnumdenbi  12763  crth  12795  phimullem  12796  setscom  13121  setsslid  13132  imasaddfnlemg  13396  imasaddflemg  13398  txbas  14981  upxp  14995  uptx  14997  txlm  15002  cnmpt21  15014  txswaphmeolem  15043  txswaphmeo  15044  comet  15222  qtopbasss  15244  cnmetdval  15252  remetdval  15270  tgqioo  15278  dvcnp2cntop  15422  dvef  15450  djucllem  16396  pwle2  16599