MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opelxpi Unicode version

Theorem opelxpi 4869
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
StepHypRef Expression
1 opelxp 4867 . 2  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  <->  ( A  e.  C  /\  B  e.  D ) )
21biimpri 198 1  |-  ( ( A  e.  C  /\  B  e.  D )  -> 
<. A ,  B >.  e.  ( C  X.  D
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721   <.cop 3777    X. cxp 4835
This theorem is referenced by:  opelvvg  4882  opelvv  4883  opbrop  4914  fliftrel  5989  fnotovb  6076  ov3  6169  ovres  6172  fovrn  6175  fnovrn  6180  ovconst2  6184  oprab2co  6391  1stconst  6394  2ndconst  6395  fnwelem  6420  opiota  6494  seqomlem2  6667  brdifun  6891  ecopqsi  6920  brecop  6956  eceqoveq  6968  th3q  6972  xpcomco  7157  xpf1o  7228  xpmapenlem  7233  unxpdomlem3  7274  fseqenlem1  7861  fseqenlem2  7862  isfin4-3  8151  axdc4lem  8291  iundom2g  8371  canthp1lem2  8484  addpiord  8717  mulpiord  8718  pinq  8760  nqereu  8762  addpipq  8770  addpqnq  8771  mulpipq  8773  mulpqnq  8774  ordpipq  8775  addpqf  8777  mulpqf  8779  recmulnq  8797  dmrecnq  8801  ltexnq  8808  enreceq  8900  0r  8911  1sr  8912  m1r  8913  addclsr  8914  mulclsr  8915  axaddf  8976  axmulf  8977  xrlenlt  9099  uzrdgfni  11253  swrdval  11719  cnrecnv  11925  ruclem1  12785  ruclem6  12789  eucalgf  13029  eucalg  13033  qredeu  13062  qnumdenbi  13091  crt  13122  phimullem  13123  prmreclem3  13241  setscom  13452  strfv2d  13454  setsid  13463  imasaddfnlem  13708  imasaddflem  13710  imasvscafn  13717  imasvscaval  13718  xpsaddlem  13755  xpsvsca  13759  xpsle  13761  comffval  13880  oppccofval  13897  isoval  13945  funcf2  14020  idfu2nd  14029  resf2nd  14047  wunfunc  14051  funcpropd  14052  fucco  14114  homaval  14141  setcco  14193  catcco  14211  xpcco  14235  xpchom2  14238  xpcco2  14239  xpccatid  14240  prfcl  14255  prf1st  14256  prf2nd  14257  catcxpccl  14259  evlf2  14270  curf1cl  14280  curf2cl  14283  curfcl  14284  uncf1  14288  uncf2  14289  uncfcurf  14291  diag11  14295  diag12  14296  diag2  14297  curf2ndf  14299  hof2fval  14307  yonedalem21  14325  yonedalem22  14330  yonedalem3b  14331  yonffthlem  14334  lsmhash  15292  efgmf  15300  efglem  15303  vrgpf  15355  vrgpinv  15356  frgpuplem  15359  frgpup2  15363  frgpnabllem1  15439  txbas  17552  txcls  17589  txcnp  17605  upxp  17608  txcnmpt  17609  uptx  17610  txlly  17621  txnlly  17622  txtube  17625  txcmplem1  17626  txlm  17633  lmcn2  17634  tx1stc  17635  txkgen  17637  xkococnlem  17644  cnmpt21  17656  txhmeo  17788  txswaphmeolem  17789  txswaphmeo  17790  ptuncnv  17792  txflf  17991  flfcnp2  17992  tmdcn2  18072  clssubg  18091  divstgplem  18103  tsmsadd  18129  imasdsf1olem  18356  xpsdsval  18364  comet  18496  txmetcnp  18530  metustidOLD  18542  metustid  18543  metustsymOLD  18544  metustsym  18545  nrmmetd  18575  isngp3  18598  ngpds  18603  tngnm  18645  qtopbaslem  18745  cnmetdval  18758  remetdval  18773  tgqioo  18784  cnheiborlem  18932  bndth  18936  htpyco2  18957  phtpyco2  18968  bcthlem5  19234  ovollb2lem  19337  ovolctb  19339  ovoliunlem2  19352  ovolscalem1  19362  ovolicc1  19365  ioombl1lem1  19405  ioorf  19418  ioorcl  19422  dyadf  19436  itg1addlem4  19544  limccnp2  19732  dvcnp2  19759  dvaddbr  19777  dvmulbr  19778  dvcobr  19785  dvef  19817  lhop1lem  19850  taylthlem2  20243  dvdsmulf1o  20932  imsdval  22131  sspval  22175  elovimad  24004  ofoprabco  24032  mbfmco2  24568  erdszelem9  24838  cvmlift2lem1  24942  cvmlift2lem9  24951  cvmlift2lem10  24952  cvmlift2lem12  24954  cvmlift2lem13  24955  cvmliftphtlem  24957  brcgr  25743  fvtransport  25870  colinearex  25898  mblfinlem  26143  areacirc  26187  opropabco  26315  heiborlem5  26414  mamudi  27329  mamudir  27330  mamuvs1  27331  mamuvs2  27332  fnotaovb  27929  aovmpt4g  27932  el2xptp0  27949  dvhelvbasei  31571  dvhopvadd  31576  dvhvaddcl  31578  dvhopvsca  31585  dvhvscacl  31586  dvhgrp  31590  dvhopclN  31596  dvhopaddN  31597  dvhopspN  31598  dib1dim2  31651  diblss  31653  diclspsn  31677  dih1dimatlem  31812
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-opab 4227  df-xp 4843
  Copyright terms: Public domain W3C validator