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

Theorem opelxpi 5030
Description: Ordered pair membership in a Cartesian 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 5028 . 2  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  <->  ( A  e.  C  /\  B  e.  D ) )
21biimpri 206 1  |-  ( ( A  e.  C  /\  B  e.  D )  -> 
<. A ,  B >.  e.  ( C  X.  D
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1767   <.cop 4033    X. cxp 4997
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-opab 4506  df-xp 5005
This theorem is referenced by:  opelvvg  5044  opelvv  5045  opbrop  5077  fliftrel  6192  elovimad  6320  fnotovb  6321  ov3  6421  ovres  6424  fovrn  6427  fnovrn  6432  ovima0  6436  ovconst2  6437  opabex2  6719  el2xptp0  6825  opiota  6840  oprab2co  6865  1stconst  6868  2ndconst  6869  fnwelem  6895  seqomlem2  7113  brdifun  7335  ecopqsi  7365  brecop  7401  eceqoveq  7413  xpcomco  7604  xpf1o  7676  xpmapenlem  7681  unxpdomlem3  7723  fseqenlem1  8401  fseqenlem2  8402  isfin4-3  8691  axdc4lem  8831  iundom2g  8911  canthp1lem2  9027  addpiord  9258  mulpiord  9259  pinq  9301  nqereu  9303  addpipq  9311  addpqnq  9312  mulpipq  9314  mulpqnq  9315  ordpipq  9316  addpqf  9318  mulpqf  9320  recmulnq  9338  dmrecnq  9342  ltexnq  9349  enreceq  9439  addsrpr  9448  mulsrpr  9449  0r  9453  1sr  9454  m1r  9455  addclsr  9456  mulclsr  9457  axaddf  9518  axmulf  9519  xrlenlt  9648  uzrdgfni  12033  swrdval  12603  cnrecnv  12957  ruclem1  13821  ruclem6  13825  eucalgf  14067  eucalg  14071  qredeu  14103  qnumdenbi  14132  crt  14163  phimullem  14164  prmreclem3  14291  setscom  14516  strfv2d  14518  setsid  14527  imasaddfnlem  14779  imasaddflem  14781  imasvscafn  14788  imasvscaval  14789  xpsaddlem  14826  xpsvsca  14830  xpsle  14832  comffval  14951  oppccofval  14968  isoval  15016  funcf2  15091  idfu2nd  15100  resf2nd  15118  wunfunc  15122  funcpropd  15123  fucco  15185  homaval  15212  setcco  15264  catcco  15282  xpcco  15306  xpchom2  15309  xpcco2  15310  xpccatid  15311  prfcl  15326  prf1st  15327  prf2nd  15328  catcxpccl  15330  evlf2  15341  curf1cl  15351  curf2cl  15354  curfcl  15355  uncf1  15359  uncf2  15360  uncfcurf  15362  diag11  15366  diag12  15367  diag2  15368  curf2ndf  15370  hof2fval  15378  yonedalem21  15396  yonedalem22  15401  yonedalem3b  15402  yonffthlem  15405  joindmss  15490  meetdmss  15504  latcl2  15531  latlem  15532  latjcom  15542  latmcom  15558  lsmhash  16519  efgmf  16527  efglem  16530  vrgpf  16582  vrgpinv  16583  frgpuplem  16586  frgpup2  16590  frgpnabllem1  16668  mamudi  18672  mamudir  18673  mamuvs1  18674  mamuvs2  18675  matsubgcell  18703  matvscacell  18705  mdetrsca  18872  pmatcoe1fsupp  18969  txbas  19803  txcls  19840  txcnp  19856  upxp  19859  txcnmpt  19860  uptx  19861  txlly  19872  txnlly  19873  txtube  19876  txcmplem1  19877  txlm  19884  lmcn2  19885  tx1stc  19886  txkgen  19888  xkococnlem  19895  cnmpt21  19907  txhmeo  20039  txswaphmeolem  20040  txswaphmeo  20041  ptuncnv  20043  txflf  20242  flfcnp2  20243  tmdcn2  20323  clssubg  20342  divstgplem  20354  tsmsadd  20384  imasdsf1olem  20611  xpsdsval  20619  comet  20751  txmetcnp  20785  metustidOLD  20797  metustid  20798  metustsymOLD  20799  metustsym  20800  nrmmetd  20830  isngp3  20853  ngpds  20858  tngnm  20900  qtopbaslem  21000  cnmetdval  21013  remetdval  21029  tgqioo  21040  cnheiborlem  21189  bndth  21193  htpyco2  21214  phtpyco2  21225  bcthlem5  21502  ovollb2lem  21634  ovolctb  21636  ovoliunlem2  21649  ovolscalem1  21659  ovolicc1  21662  ioombl1lem1  21703  ioorf  21717  ioorcl  21721  dyadf  21735  itg1addlem4  21841  limccnp2  22031  dvcnp2  22058  dvaddbr  22076  dvmulbr  22077  dvcobr  22084  dvef  22116  lhop1lem  22149  taylthlem2  22503  dvdsmulf1o  23198  tgelrnln  23724  tghilbert1_1  23731  brcgr  23879  imsdval  25268  sspval  25312  ofoprabco  27177  f1od2  27219  fimaproj  27499  prsdm  27532  prsrn  27533  qtophaus  27637  mbfmco2  27876  eulerpartlemgh  27957  afsval  28191  erdszelem9  28283  cvmlift2lem1  28387  cvmlift2lem9  28396  cvmlift2lem10  28397  cvmlift2lem12  28399  cvmlift2lem13  28400  cvmliftphtlem  28402  fvtransport  29259  colinearex  29287  finixpnum  29615  heicant  29626  mblfinlem1  29628  mblfinlem2  29629  ftc1anc  29675  areacirc  29689  opropabco  29817  heiborlem5  29914  fnotaovb  31750  aovmpt4g  31753  dvhelvbasei  35885  dvhopvadd  35890  dvhvaddcl  35892  dvhopvsca  35899  dvhvscacl  35900  dvhgrp  35904  dvhopclN  35910  dvhopaddN  35911  dvhopspN  35912  dib1dim2  35965  diblss  35967  diclspsn  35991  dih1dimatlem  36126
  Copyright terms: Public domain W3C validator