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

Theorem opelxpi 4821
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 4819 . 2  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  <->  ( A  e.  C  /\  B  e.  D ) )
21biimpri 209 1  |-  ( ( A  e.  C  /\  B  e.  D )  -> 
<. A ,  B >.  e.  ( C  X.  D
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    e. wcel 1872   <.cop 3940    X. cxp 4787
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402  ax-sep 4482  ax-nul 4491  ax-pr 4596
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-ne 2595  df-ral 2713  df-rex 2714  df-rab 2717  df-v 3018  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3698  df-if 3848  df-sn 3935  df-pr 3937  df-op 3941  df-opab 4419  df-xp 4795
This theorem is referenced by:  opelvvg  4835  opelvv  4836  opbrop  4869  fpr2g  6077  fliftrel  6153  elovimad  6282  fnotovb  6283  ov3  6384  ovres  6387  fovrn  6390  fnovrn  6395  ovima0  6399  ovconst2  6400  opabex2  6682  el2xptp0  6788  opiota  6803  oprab2co  6829  1stconst  6832  2ndconst  6833  fnwelem  6859  seqomlem2  7116  brdifun  7338  ecopqsi  7368  brecop  7404  eceqoveq  7416  xpcomco  7608  xpf1o  7680  xpmapenlem  7685  unxpdomlem3  7724  fseqenlem1  8399  fseqenlem2  8400  isfin4-3  8689  axdc4lem  8829  iundom2g  8909  canthp1lem2  9022  addpiord  9253  mulpiord  9254  pinq  9296  nqereu  9298  addpipq  9306  addpqnq  9307  mulpipq  9309  mulpqnq  9310  ordpipq  9311  addpqf  9313  mulpqf  9315  recmulnq  9333  dmrecnq  9337  ltexnq  9344  enreceq  9434  addsrpr  9443  mulsrpr  9444  0r  9448  1sr  9449  m1r  9450  addclsr  9451  mulclsr  9452  axaddf  9513  axmulf  9514  xrlenlt  9643  uzrdgfni  12115  swrdval  12712  cnrecnv  13165  ruclem1  14219  ruclem6  14223  eucalgf  14478  eucalg  14482  qredeu  14600  qnumdenbi  14629  crt  14662  phimullem  14663  prmreclem3  14798  setscom  15089  strfv2d  15091  setsid  15100  imasaddfnlem  15370  imasaddflem  15372  imasvscafn  15379  imasvscaval  15380  xpsaddlem  15417  xpsvsca  15421  xpsle  15423  comffval  15540  oppccofval  15557  isoval  15606  funcf2  15709  idfu2nd  15718  resf2nd  15736  wunfunc  15740  funcpropd  15741  fucco  15803  homaval  15862  setcco  15914  catcco  15932  estrcco  15951  xpcco  16004  xpchom2  16007  xpcco2  16008  xpccatid  16009  prfcl  16024  prf1st  16025  prf2nd  16026  catcxpccl  16028  evlf2  16039  curf1cl  16049  curf2cl  16052  curfcl  16053  uncf1  16057  uncf2  16058  uncfcurf  16060  diag11  16064  diag12  16065  diag2  16066  curf2ndf  16068  hof2fval  16076  yonedalem21  16094  yonedalem22  16099  yonedalem3b  16100  yonffthlem  16103  joindmss  16189  meetdmss  16203  latcl2  16230  latlem  16231  latjcom  16241  latmcom  16257  lsmhash  17291  efgmf  17299  efglem  17302  vrgpf  17354  vrgpinv  17355  frgpuplem  17358  frgpup2  17362  frgpnabllem1  17445  mamudi  19363  mamudir  19364  mamuvs1  19365  mamuvs2  19366  matsubgcell  19394  matvscacell  19396  mdetrsca  19563  pmatcoe1fsupp  19660  txbas  20517  txcls  20554  txcnp  20570  upxp  20573  txcnmpt  20574  uptx  20575  txlly  20586  txnlly  20587  txtube  20590  txcmplem1  20591  txlm  20598  lmcn2  20599  tx1stc  20600  txkgen  20602  xkococnlem  20609  cnmpt21  20621  txhmeo  20753  txswaphmeolem  20754  txswaphmeo  20755  ptuncnv  20757  txflf  20956  flfcnp2  20957  tmdcn2  21039  clssubg  21058  qustgplem  21070  tsmsadd  21096  imasdsf1olem  21323  xpsdsval  21331  comet  21463  txmetcnp  21497  metustid  21504  metustsym  21505  nrmmetd  21524  isngp3  21547  ngpds  21552  tngnm  21594  qtopbaslem  21714  cnmetdval  21726  remetdval  21742  tgqioo  21753  cnheiborlem  21917  bndth  21921  htpyco2  21945  phtpyco2  21956  bcthlem5  22231  ovollb2lem  22376  ovolctb  22378  ovoliunlem2  22391  ovolscalem1  22401  ovolicc1  22404  ioombl1lem1  22446  ioorf  22460  ioorcl  22464  ioorfOLD  22465  ioorclOLD  22469  dyadf  22484  itg1addlem4  22592  limccnp2  22782  dvcnp2  22809  dvaddbr  22827  dvmulbr  22828  dvcobr  22835  dvef  22867  lhop1lem  22900  taylthlem2  23264  dvdsmulf1o  24058  tgelrnln  24610  brcgr  24865  imsdval  26253  sspval  26297  ofoprabco  28206  f1od2  28252  fimaproj  28605  qtophaus  28608  prsdm  28665  prsrn  28666  mbfmco2  29032  eulerpartlemgh  29156  afsval  29433  erdszelem9  29867  cvmlift2lem1  29970  cvmlift2lem9  29979  cvmlift2lem10  29980  cvmlift2lem12  29982  cvmlift2lem13  29983  cvmliftphtlem  29985  msubco  30114  msubff1  30139  mvhf  30141  msubvrs  30143  fvtransport  30741  colinearex  30769  icoreunrn  31663  relowlpssretop  31668  finixpnum  31831  poimirlem3  31844  poimirlem4  31845  poimirlem15  31856  poimirlem17  31858  poimirlem20  31861  poimirlem25  31866  poimirlem26  31867  poimirlem27  31868  heicant  31876  mblfinlem1  31878  mblfinlem2  31879  ftc1anc  31926  areacirc  31938  opropabco  31951  heiborlem5  32048  dvhelvbasei  34562  dvhopvadd  34567  dvhvaddcl  34569  dvhopvsca  34576  dvhvscacl  34577  dvhgrp  34581  dvhopclN  34587  dvhopaddN  34588  dvhopspN  34589  dib1dim2  34642  diblss  34644  diclspsn  34668  dih1dimatlem  34803  projf1o  37372  hoicvr  38211  hoicvrrex  38219  ovnsubaddlem1  38233  ovnhoilem1  38264  fnotaovb  38507  aovmpt4g  38510  rngccoALTV  39575  ringccoALTV  39638  rhmsubclem2  39674  rhmsubcALTVlem2  39693
  Copyright terms: Public domain W3C validator