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

Theorem opelxpi 4886
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 4884 . 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 1870   <.cop 4008    X. cxp 4852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pr 4661
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-opab 4485  df-xp 4860
This theorem is referenced by:  opelvvg  4900  opelvv  4901  opbrop  4934  fpr2g  6140  fliftrel  6216  elovimad  6345  fnotovb  6346  ov3  6447  ovres  6450  fovrn  6453  fnovrn  6458  ovima0  6462  ovconst2  6463  opabex2  6745  el2xptp0  6851  opiota  6866  oprab2co  6892  1stconst  6895  2ndconst  6896  fnwelem  6922  seqomlem2  7176  brdifun  7398  ecopqsi  7428  brecop  7464  eceqoveq  7476  xpcomco  7668  xpf1o  7740  xpmapenlem  7745  unxpdomlem3  7784  fseqenlem1  8453  fseqenlem2  8454  isfin4-3  8743  axdc4lem  8883  iundom2g  8963  canthp1lem2  9077  addpiord  9308  mulpiord  9309  pinq  9351  nqereu  9353  addpipq  9361  addpqnq  9362  mulpipq  9364  mulpqnq  9365  ordpipq  9366  addpqf  9368  mulpqf  9370  recmulnq  9388  dmrecnq  9392  ltexnq  9399  enreceq  9489  addsrpr  9498  mulsrpr  9499  0r  9503  1sr  9504  m1r  9505  addclsr  9506  mulclsr  9507  axaddf  9568  axmulf  9569  xrlenlt  9698  uzrdgfni  12169  swrdval  12758  cnrecnv  13207  ruclem1  14261  ruclem6  14265  eucalgf  14513  eucalg  14517  qredeu  14635  qnumdenbi  14664  crt  14695  phimullem  14696  prmreclem3  14825  setscom  15116  strfv2d  15118  setsid  15127  imasaddfnlem  15385  imasaddflem  15387  imasvscafn  15394  imasvscaval  15395  xpsaddlem  15432  xpsvsca  15436  xpsle  15438  comffval  15555  oppccofval  15572  isoval  15621  funcf2  15724  idfu2nd  15733  resf2nd  15751  wunfunc  15755  funcpropd  15756  fucco  15818  homaval  15877  setcco  15929  catcco  15947  estrcco  15966  xpcco  16019  xpchom2  16022  xpcco2  16023  xpccatid  16024  prfcl  16039  prf1st  16040  prf2nd  16041  catcxpccl  16043  evlf2  16054  curf1cl  16064  curf2cl  16067  curfcl  16068  uncf1  16072  uncf2  16073  uncfcurf  16075  diag11  16079  diag12  16080  diag2  16081  curf2ndf  16083  hof2fval  16091  yonedalem21  16109  yonedalem22  16114  yonedalem3b  16115  yonffthlem  16118  joindmss  16204  meetdmss  16218  latcl2  16245  latlem  16246  latjcom  16256  latmcom  16272  lsmhash  17290  efgmf  17298  efglem  17301  vrgpf  17353  vrgpinv  17354  frgpuplem  17357  frgpup2  17361  frgpnabllem1  17444  mamudi  19359  mamudir  19360  mamuvs1  19361  mamuvs2  19362  matsubgcell  19390  matvscacell  19392  mdetrsca  19559  pmatcoe1fsupp  19656  txbas  20513  txcls  20550  txcnp  20566  upxp  20569  txcnmpt  20570  uptx  20571  txlly  20582  txnlly  20583  txtube  20586  txcmplem1  20587  txlm  20594  lmcn2  20595  tx1stc  20596  txkgen  20598  xkococnlem  20605  cnmpt21  20617  txhmeo  20749  txswaphmeolem  20750  txswaphmeo  20751  ptuncnv  20753  txflf  20952  flfcnp2  20953  tmdcn2  21035  clssubg  21054  qustgplem  21066  tsmsadd  21092  imasdsf1olem  21319  xpsdsval  21327  comet  21459  txmetcnp  21493  metustid  21500  metustsym  21501  nrmmetd  21520  isngp3  21543  ngpds  21548  tngnm  21590  qtopbaslem  21690  cnmetdval  21702  remetdval  21718  tgqioo  21729  cnheiborlem  21878  bndth  21882  htpyco2  21903  phtpyco2  21914  bcthlem5  22189  ovollb2lem  22319  ovolctb  22321  ovoliunlem2  22334  ovolscalem1  22344  ovolicc1  22347  ioombl1lem1  22388  ioorf  22402  ioorcl  22406  ioorfOLD  22407  ioorclOLD  22411  dyadf  22426  itg1addlem4  22534  limccnp2  22724  dvcnp2  22751  dvaddbr  22769  dvmulbr  22770  dvcobr  22777  dvef  22809  lhop1lem  22842  taylthlem2  23194  dvdsmulf1o  23986  tgelrnln  24534  brcgr  24776  imsdval  26163  sspval  26207  ofoprabco  28107  f1od2  28152  fimaproj  28499  qtophaus  28502  prsdm  28559  prsrn  28560  mbfmco2  28926  eulerpartlemgh  29037  afsval  29276  erdszelem9  29710  cvmlift2lem1  29813  cvmlift2lem9  29822  cvmlift2lem10  29823  cvmlift2lem12  29825  cvmlift2lem13  29826  cvmliftphtlem  29828  msubco  29957  msubff1  29982  mvhf  29984  msubvrs  29986  fvtransport  30584  colinearex  30612  icoreunrn  31496  relowlpssretop  31501  finixpnum  31634  poimirlem3  31647  poimirlem4  31648  poimirlem15  31659  poimirlem17  31661  poimirlem20  31664  poimirlem25  31669  poimirlem26  31670  poimirlem27  31671  heicant  31679  mblfinlem1  31681  mblfinlem2  31682  ftc1anc  31729  areacirc  31741  opropabco  31754  heiborlem5  31851  dvhelvbasei  34365  dvhopvadd  34370  dvhvaddcl  34372  dvhopvsca  34379  dvhvscacl  34380  dvhgrp  34384  dvhopclN  34390  dvhopaddN  34391  dvhopspN  34392  dib1dim2  34445  diblss  34447  diclspsn  34471  dih1dimatlem  34606  fnotaovb  38090  aovmpt4g  38093  rngccoALTV  38748  ringccoALTV  38811  rhmsubclem2  38847  rhmsubcALTVlem2  38866
  Copyright terms: Public domain W3C validator