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

Theorem opelxpi 4737
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 4735 . 2  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  <->  ( A  e.  C  /\  B  e.  D ) )
21biimpri 197 1  |-  ( ( A  e.  C  /\  B  e.  D )  -> 
<. A ,  B >.  e.  ( C  X.  D
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1696   <.cop 3656    X. cxp 4703
This theorem is referenced by:  opelvvg  4750  opelvv  4751  opbrop  4783  fliftrel  5823  fnotovb  5910  ov3  6000  ovres  6003  fovrn  6006  fnovrn  6011  ovconst2  6015  oprab2co  6220  1stconst  6223  2ndconst  6224  fnwelem  6246  opiota  6306  seqomlem2  6479  brdifun  6703  ecopqsi  6732  brecop  6767  eceqoveq  6779  th3q  6783  xpcomco  6968  xpf1o  7039  xpmapenlem  7044  unxpdomlem3  7085  fseqenlem1  7667  fseqenlem2  7668  isfin4-3  7957  axdc4lem  8097  iundom2g  8178  canthp1lem2  8291  addpiord  8524  mulpiord  8525  pinq  8567  nqereu  8569  addpipq  8577  addpqnq  8578  mulpipq  8580  mulpqnq  8581  ordpipq  8582  addpqf  8584  mulpqf  8586  recmulnq  8604  dmrecnq  8608  ltexnq  8615  enreceq  8707  0r  8718  1sr  8719  m1r  8720  addclsr  8721  mulclsr  8722  axaddf  8783  axmulf  8784  xrlenlt  8906  uzrdgfni  11037  swrdval  11466  cnrecnv  11666  ruclem1  12525  ruclem6  12529  eucalgf  12769  eucalg  12773  qredeu  12802  qnumdenbi  12831  crt  12862  phimullem  12863  prmreclem3  12981  setscom  13192  strfv2d  13194  setsid  13203  imasaddfnlem  13446  imasaddflem  13448  imasvscafn  13455  imasvscaval  13456  xpsaddlem  13493  xpsvsca  13497  xpsle  13499  comffval  13618  oppccofval  13635  isoval  13683  funcf2  13758  idfu2nd  13767  resf2nd  13785  wunfunc  13789  funcpropd  13790  fucco  13852  homaval  13879  setcco  13931  catcco  13949  xpcco  13973  xpchom2  13976  xpcco2  13977  xpccatid  13978  prfcl  13993  prf1st  13994  prf2nd  13995  catcxpccl  13997  evlf2  14008  curf1cl  14018  curf2cl  14021  curfcl  14022  uncf1  14026  uncf2  14027  uncfcurf  14029  diag11  14033  diag12  14034  diag2  14035  curf2ndf  14037  hof2fval  14045  yonedalem21  14063  yonedalem22  14068  yonedalem3b  14069  yonffthlem  14072  lsmhash  15030  efgmf  15038  efglem  15041  vrgpf  15093  vrgpinv  15094  frgpuplem  15097  frgpup2  15101  frgpnabllem1  15177  txbas  17278  txcls  17315  txcnp  17330  upxp  17333  txcnmpt  17334  uptx  17335  txlly  17346  txnlly  17347  txtube  17350  txcmplem1  17351  txlm  17358  lmcn2  17359  tx1stc  17360  txkgen  17362  xkococnlem  17369  cnmpt21  17381  txhmeo  17510  txswaphmeolem  17511  txswaphmeo  17512  ptuncnv  17514  txflf  17717  flfcnp2  17718  tmdcn2  17788  clssubg  17807  divstgplem  17819  tsmsadd  17845  imasdsf1olem  17953  xpsdsval  17961  comet  18075  txmetcnp  18109  nrmmetd  18113  isngp3  18136  ngpds  18141  tngnm  18183  qtopbaslem  18283  cnmetdval  18296  remetdval  18311  tgqioo  18322  cnheiborlem  18468  bndth  18472  htpyco2  18493  phtpyco2  18504  bcthlem5  18766  ovollb2lem  18863  ovolctb  18865  ovoliunlem2  18878  ovolscalem1  18888  ovolicc1  18891  ioombl1lem1  18931  ioorf  18944  ioorcl  18948  dyadf  18962  itg1addlem4  19070  limccnp2  19258  dvcnp2  19285  dvaddbr  19303  dvmulbr  19304  dvcobr  19311  dvef  19343  lhop1lem  19376  taylthlem2  19769  dvdsmulf1o  20450  imsdval  21271  sspval  21315  elovimad  23220  ofoprabco  23247  mbfmco2  23585  erdszelem9  23745  cvmlift2lem1  23848  cvmlift2lem9  23857  cvmlift2lem10  23858  cvmlift2lem12  23860  cvmlift2lem13  23861  cvmliftphtlem  23863  brcgr  24600  fvtransport  24727  colinearex  24755  areacirc  25034  stcat  25147  ltrcmp  25508  prdnei  25676  limptlimpr2lem2  25678  opropabco  26492  heiborlem5  26642  mamudi  27564  mamudir  27565  mamuvs1  27566  mamuvs2  27567  fnotaovb  28166  aovmpt4g  28169  dvhelvbasei  31900  dvhopvadd  31905  dvhvaddcl  31907  dvhopvsca  31914  dvhvscacl  31915  dvhgrp  31919  dvhopclN  31925  dvhopaddN  31926  dvhopspN  31927  dib1dim2  31980  diblss  31982  diclspsn  32006  dih1dimatlem  32141
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-opab 4094  df-xp 4711
  Copyright terms: Public domain W3C validator