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

Theorem opelxpi 4912
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 4910 . 2  |-  ( <. A ,  B >.  e.  ( C  X.  D
)  <->  ( A  e.  C  /\  B  e.  D ) )
21biimpri 199 1  |-  ( ( A  e.  C  /\  B  e.  D )  -> 
<. A ,  B >.  e.  ( C  X.  D
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    e. wcel 1726   <.cop 3819    X. cxp 4878
This theorem is referenced by:  opelvvg  4925  opelvv  4926  opbrop  4957  fliftrel  6032  fnotovb  6119  ov3  6212  ovres  6215  fovrn  6218  fnovrn  6223  ovconst2  6227  oprab2co  6434  1stconst  6437  2ndconst  6438  fnwelem  6463  opiota  6537  seqomlem2  6710  brdifun  6934  ecopqsi  6963  brecop  6999  eceqoveq  7011  th3q  7015  xpcomco  7200  xpf1o  7271  xpmapenlem  7276  unxpdomlem3  7317  fseqenlem1  7907  fseqenlem2  7908  isfin4-3  8197  axdc4lem  8337  iundom2g  8417  canthp1lem2  8530  addpiord  8763  mulpiord  8764  pinq  8806  nqereu  8808  addpipq  8816  addpqnq  8817  mulpipq  8819  mulpqnq  8820  ordpipq  8821  addpqf  8823  mulpqf  8825  recmulnq  8843  dmrecnq  8847  ltexnq  8854  enreceq  8946  0r  8957  1sr  8958  m1r  8959  addclsr  8960  mulclsr  8961  axaddf  9022  axmulf  9023  xrlenlt  9145  uzrdgfni  11300  swrdval  11766  cnrecnv  11972  ruclem1  12832  ruclem6  12836  eucalgf  13076  eucalg  13080  qredeu  13109  qnumdenbi  13138  crt  13169  phimullem  13170  prmreclem3  13288  setscom  13499  strfv2d  13501  setsid  13510  imasaddfnlem  13755  imasaddflem  13757  imasvscafn  13764  imasvscaval  13765  xpsaddlem  13802  xpsvsca  13806  xpsle  13808  comffval  13927  oppccofval  13944  isoval  13992  funcf2  14067  idfu2nd  14076  resf2nd  14094  wunfunc  14098  funcpropd  14099  fucco  14161  homaval  14188  setcco  14240  catcco  14258  xpcco  14282  xpchom2  14285  xpcco2  14286  xpccatid  14287  prfcl  14302  prf1st  14303  prf2nd  14304  catcxpccl  14306  evlf2  14317  curf1cl  14327  curf2cl  14330  curfcl  14331  uncf1  14335  uncf2  14336  uncfcurf  14338  diag11  14342  diag12  14343  diag2  14344  curf2ndf  14346  hof2fval  14354  yonedalem21  14372  yonedalem22  14377  yonedalem3b  14378  yonffthlem  14381  lsmhash  15339  efgmf  15347  efglem  15350  vrgpf  15402  vrgpinv  15403  frgpuplem  15406  frgpup2  15410  frgpnabllem1  15486  txbas  17601  txcls  17638  txcnp  17654  upxp  17657  txcnmpt  17658  uptx  17659  txlly  17670  txnlly  17671  txtube  17674  txcmplem1  17675  txlm  17682  lmcn2  17683  tx1stc  17684  txkgen  17686  xkococnlem  17693  cnmpt21  17705  txhmeo  17837  txswaphmeolem  17838  txswaphmeo  17839  ptuncnv  17841  txflf  18040  flfcnp2  18041  tmdcn2  18121  clssubg  18140  divstgplem  18152  tsmsadd  18178  imasdsf1olem  18405  xpsdsval  18413  comet  18545  txmetcnp  18579  metustidOLD  18591  metustid  18592  metustsymOLD  18593  metustsym  18594  nrmmetd  18624  isngp3  18647  ngpds  18652  tngnm  18694  qtopbaslem  18794  cnmetdval  18807  remetdval  18822  tgqioo  18833  cnheiborlem  18981  bndth  18985  htpyco2  19006  phtpyco2  19017  bcthlem5  19283  ovollb2lem  19386  ovolctb  19388  ovoliunlem2  19401  ovolscalem1  19411  ovolicc1  19414  ioombl1lem1  19454  ioorf  19467  ioorcl  19471  dyadf  19485  itg1addlem4  19593  limccnp2  19781  dvcnp2  19808  dvaddbr  19826  dvmulbr  19827  dvcobr  19834  dvef  19866  lhop1lem  19899  taylthlem2  20292  dvdsmulf1o  20981  imsdval  22180  sspval  22224  elovimad  24053  ofoprabco  24081  mbfmco2  24617  erdszelem9  24887  cvmlift2lem1  24991  cvmlift2lem9  25000  cvmlift2lem10  25001  cvmlift2lem12  25003  cvmlift2lem13  25004  cvmliftphtlem  25006  brcgr  25841  fvtransport  25968  colinearex  25996  mblfinlem1  26245  mblfinlem2  26246  ftc1anc  26290  areacirc  26299  opropabco  26427  heiborlem5  26526  mamudi  27440  mamudir  27441  mamuvs1  27442  mamuvs2  27443  fnotaovb  28040  aovmpt4g  28043  el2xptp0  28064  dvhelvbasei  31948  dvhopvadd  31953  dvhvaddcl  31955  dvhopvsca  31962  dvhvscacl  31963  dvhgrp  31967  dvhopclN  31973  dvhopaddN  31974  dvhopspN  31975  dib1dim2  32028  diblss  32030  diclspsn  32054  dih1dimatlem  32189
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pr 4405
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-opab 4269  df-xp 4886
  Copyright terms: Public domain W3C validator