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

Theorem opelxpi 4721
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 4719 . 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 1684   <.cop 3643    X. cxp 4687
This theorem is referenced by:  opelvvg  4734  opelvv  4735  opbrop  4767  fliftrel  5807  fnotovb  5894  ov3  5984  ovres  5987  fovrn  5990  fnovrn  5995  ovconst2  5999  oprab2co  6204  1stconst  6207  2ndconst  6208  fnwelem  6230  opiota  6290  seqomlem2  6463  brdifun  6687  ecopqsi  6716  brecop  6751  eceqoveq  6763  th3q  6767  xpcomco  6952  xpf1o  7023  xpmapenlem  7028  unxpdomlem3  7069  fseqenlem1  7651  fseqenlem2  7652  isfin4-3  7941  axdc4lem  8081  iundom2g  8162  canthp1lem2  8275  addpiord  8508  mulpiord  8509  pinq  8551  nqereu  8553  addpipq  8561  addpqnq  8562  mulpipq  8564  mulpqnq  8565  ordpipq  8566  addpqf  8568  mulpqf  8570  recmulnq  8588  dmrecnq  8592  ltexnq  8599  enreceq  8691  0r  8702  1sr  8703  m1r  8704  addclsr  8705  mulclsr  8706  axaddf  8767  axmulf  8768  xrlenlt  8890  uzrdgfni  11021  swrdval  11450  cnrecnv  11650  ruclem1  12509  ruclem6  12513  eucalgf  12753  eucalg  12757  qredeu  12786  qnumdenbi  12815  crt  12846  phimullem  12847  prmreclem3  12965  setscom  13176  strfv2d  13178  setsid  13187  imasaddfnlem  13430  imasaddflem  13432  imasvscafn  13439  imasvscaval  13440  xpsaddlem  13477  xpsvsca  13481  xpsle  13483  comffval  13602  oppccofval  13619  isoval  13667  funcf2  13742  idfu2nd  13751  resf2nd  13769  wunfunc  13773  funcpropd  13774  fucco  13836  homaval  13863  setcco  13915  catcco  13933  xpcco  13957  xpchom2  13960  xpcco2  13961  xpccatid  13962  prfcl  13977  prf1st  13978  prf2nd  13979  catcxpccl  13981  evlf2  13992  curf1cl  14002  curf2cl  14005  curfcl  14006  uncf1  14010  uncf2  14011  uncfcurf  14013  diag11  14017  diag12  14018  diag2  14019  curf2ndf  14021  hof2fval  14029  yonedalem21  14047  yonedalem22  14052  yonedalem3b  14053  yonffthlem  14056  lsmhash  15014  efgmf  15022  efglem  15025  vrgpf  15077  vrgpinv  15078  frgpuplem  15081  frgpup2  15085  frgpnabllem1  15161  txbas  17262  txcls  17299  txcnp  17314  upxp  17317  txcnmpt  17318  uptx  17319  txlly  17330  txnlly  17331  txtube  17334  txcmplem1  17335  txlm  17342  lmcn2  17343  tx1stc  17344  txkgen  17346  xkococnlem  17353  cnmpt21  17365  txhmeo  17494  txswaphmeolem  17495  txswaphmeo  17496  ptuncnv  17498  txflf  17701  flfcnp2  17702  tmdcn2  17772  clssubg  17791  divstgplem  17803  tsmsadd  17829  imasdsf1olem  17937  xpsdsval  17945  comet  18059  txmetcnp  18093  nrmmetd  18097  isngp3  18120  ngpds  18125  tngnm  18167  qtopbaslem  18267  cnmetdval  18280  remetdval  18295  tgqioo  18306  cnheiborlem  18452  bndth  18456  htpyco2  18477  phtpyco2  18488  bcthlem5  18750  ovollb2lem  18847  ovolctb  18849  ovoliunlem2  18862  ovolscalem1  18872  ovolicc1  18875  ioombl1lem1  18915  ioorf  18928  ioorcl  18932  dyadf  18946  itg1addlem4  19054  limccnp2  19242  dvcnp2  19269  dvaddbr  19287  dvmulbr  19288  dvcobr  19295  dvef  19327  lhop1lem  19360  taylthlem2  19753  dvdsmulf1o  20434  imsdval  21255  sspval  21299  elovimad  23205  ofoprabco  23232  mbfmco2  23570  erdszelem9  23730  cvmlift2lem1  23833  cvmlift2lem9  23842  cvmlift2lem10  23843  cvmlift2lem12  23845  cvmlift2lem13  23846  cvmliftphtlem  23848  funpartfv  24483  brcgr  24528  fvtransport  24655  colinearex  24683  areacirc  24931  stcat  25044  ltrcmp  25405  prdnei  25573  limptlimpr2lem2  25575  opropabco  26389  heiborlem5  26539  mamudi  27461  mamudir  27462  mamuvs1  27463  mamuvs2  27464  fnotaovb  28058  aovmpt4g  28061  dvhelvbasei  31278  dvhopvadd  31283  dvhvaddcl  31285  dvhopvsca  31292  dvhvscacl  31293  dvhgrp  31297  dvhopclN  31303  dvhopaddN  31304  dvhopspN  31305  dib1dim2  31358  diblss  31360  diclspsn  31384  dih1dimatlem  31519
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-opab 4078  df-xp 4695
  Copyright terms: Public domain W3C validator