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

Theorem opelxpi 4980
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 4978 . 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 1758   <.cop 3992    X. cxp 4947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4522  ax-nul 4530  ax-pr 4640
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-rab 2808  df-v 3080  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3747  df-if 3901  df-sn 3987  df-pr 3989  df-op 3993  df-opab 4460  df-xp 4955
This theorem is referenced by:  opelvvg  4993  opelvv  4994  opbrop  5025  fliftrel  6111  fnotovb  6239  ov3  6338  ovres  6341  fovrn  6344  fnovrn  6349  ovima0  6353  ovconst2  6354  opabex2  6627  opiota  6744  oprab2co  6769  1stconst  6772  2ndconst  6773  fnwelem  6798  seqomlem2  7017  brdifun  7239  ecopqsi  7268  brecop  7304  eceqoveq  7316  th3q  7320  xpcomco  7512  xpf1o  7584  xpmapenlem  7589  unxpdomlem3  7631  fseqenlem1  8306  fseqenlem2  8307  isfin4-3  8596  axdc4lem  8736  iundom2g  8816  canthp1lem2  8932  addpiord  9165  mulpiord  9166  pinq  9208  nqereu  9210  addpipq  9218  addpqnq  9219  mulpipq  9221  mulpqnq  9222  ordpipq  9223  addpqf  9225  mulpqf  9227  recmulnq  9245  dmrecnq  9249  ltexnq  9256  enreceq  9348  0r  9359  1sr  9360  m1r  9361  addclsr  9362  mulclsr  9363  axaddf  9424  axmulf  9425  xrlenlt  9554  uzrdgfni  11899  swrdval  12432  cnrecnv  12773  ruclem1  13632  ruclem6  13636  eucalgf  13877  eucalg  13881  qredeu  13912  qnumdenbi  13941  crt  13972  phimullem  13973  prmreclem3  14098  setscom  14323  strfv2d  14325  setsid  14334  imasaddfnlem  14586  imasaddflem  14588  imasvscafn  14595  imasvscaval  14596  xpsaddlem  14633  xpsvsca  14637  xpsle  14639  comffval  14758  oppccofval  14775  isoval  14823  funcf2  14898  idfu2nd  14907  resf2nd  14925  wunfunc  14929  funcpropd  14930  fucco  14992  homaval  15019  setcco  15071  catcco  15089  xpcco  15113  xpchom2  15116  xpcco2  15117  xpccatid  15118  prfcl  15133  prf1st  15134  prf2nd  15135  catcxpccl  15137  evlf2  15148  curf1cl  15158  curf2cl  15161  curfcl  15162  uncf1  15166  uncf2  15167  uncfcurf  15169  diag11  15173  diag12  15174  diag2  15175  curf2ndf  15177  hof2fval  15185  yonedalem21  15203  yonedalem22  15208  yonedalem3b  15209  yonffthlem  15212  joindmss  15297  meetdmss  15311  latcl2  15338  latlem  15339  latjcom  15349  latmcom  15365  lsmhash  16324  efgmf  16332  efglem  16335  vrgpf  16387  vrgpinv  16388  frgpuplem  16391  frgpup2  16395  frgpnabllem1  16473  mamudi  18433  mamudir  18434  mamuvs1  18435  mamuvs2  18436  mdetrsca  18542  txbas  19273  txcls  19310  txcnp  19326  upxp  19329  txcnmpt  19330  uptx  19331  txlly  19342  txnlly  19343  txtube  19346  txcmplem1  19347  txlm  19354  lmcn2  19355  tx1stc  19356  txkgen  19358  xkococnlem  19365  cnmpt21  19377  txhmeo  19509  txswaphmeolem  19510  txswaphmeo  19511  ptuncnv  19513  txflf  19712  flfcnp2  19713  tmdcn2  19793  clssubg  19812  divstgplem  19824  tsmsadd  19854  imasdsf1olem  20081  xpsdsval  20089  comet  20221  txmetcnp  20255  metustidOLD  20267  metustid  20268  metustsymOLD  20269  metustsym  20270  nrmmetd  20300  isngp3  20323  ngpds  20328  tngnm  20370  qtopbaslem  20470  cnmetdval  20483  remetdval  20499  tgqioo  20510  cnheiborlem  20659  bndth  20663  htpyco2  20684  phtpyco2  20695  bcthlem5  20972  ovollb2lem  21104  ovolctb  21106  ovoliunlem2  21119  ovolscalem1  21129  ovolicc1  21132  ioombl1lem1  21173  ioorf  21187  ioorcl  21191  dyadf  21205  itg1addlem4  21311  limccnp2  21501  dvcnp2  21528  dvaddbr  21546  dvmulbr  21547  dvcobr  21554  dvef  21586  lhop1lem  21619  taylthlem2  21973  dvdsmulf1o  22668  tgelrnln  23176  tghilbert1_1  23183  brcgr  23299  imsdval  24230  sspval  24274  elovimad  26108  ofoprabco  26134  f1od2  26176  prsdm  26490  prsrn  26491  mbfmco2  26825  eulerpartlemgh  26906  afsval  27140  erdszelem9  27232  cvmlift2lem1  27336  cvmlift2lem9  27345  cvmlift2lem10  27346  cvmlift2lem12  27348  cvmlift2lem13  27349  cvmliftphtlem  27351  fvtransport  28208  colinearex  28236  finixpnum  28563  heicant  28575  mblfinlem1  28577  mblfinlem2  28578  ftc1anc  28624  areacirc  28638  opropabco  28766  heiborlem5  28863  fnotaovb  30253  aovmpt4g  30256  el2xptp0  30276  matsubgcell  31019  matvscacell  31022  pmatcoe1fsupp  31193  dvhelvbasei  35072  dvhopvadd  35077  dvhvaddcl  35079  dvhopvsca  35086  dvhvscacl  35087  dvhgrp  35091  dvhopclN  35097  dvhopaddN  35098  dvhopspN  35099  dib1dim2  35152  diblss  35154  diclspsn  35178  dih1dimatlem  35313
  Copyright terms: Public domain W3C validator