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

Theorem opelxpi 4858
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 4856 . 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 1755   <.cop 3871    X. cxp 4825
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-opab 4339  df-xp 4833
This theorem is referenced by:  opelvvg  4871  opelvv  4872  opbrop  4903  fliftrel  5988  fnotovb  6118  ov3  6216  ovres  6219  fovrn  6222  fnovrn  6227  ovima0  6231  ovconst2  6232  opabex2  6505  opiota  6622  oprab2co  6647  1stconst  6650  2ndconst  6651  fnwelem  6676  seqomlem2  6892  brdifun  7116  ecopqsi  7145  brecop  7181  eceqoveq  7193  th3q  7197  xpcomco  7389  xpf1o  7461  xpmapenlem  7466  unxpdomlem3  7507  fseqenlem1  8182  fseqenlem2  8183  isfin4-3  8472  axdc4lem  8612  iundom2g  8692  canthp1lem2  8808  addpiord  9041  mulpiord  9042  pinq  9084  nqereu  9086  addpipq  9094  addpqnq  9095  mulpipq  9097  mulpqnq  9098  ordpipq  9099  addpqf  9101  mulpqf  9103  recmulnq  9121  dmrecnq  9125  ltexnq  9132  enreceq  9224  0r  9235  1sr  9236  m1r  9237  addclsr  9238  mulclsr  9239  axaddf  9300  axmulf  9301  xrlenlt  9430  uzrdgfni  11765  swrdval  12297  cnrecnv  12638  ruclem1  13496  ruclem6  13500  eucalgf  13741  eucalg  13745  qredeu  13776  qnumdenbi  13805  crt  13836  phimullem  13837  prmreclem3  13962  setscom  14187  strfv2d  14189  setsid  14198  imasaddfnlem  14449  imasaddflem  14451  imasvscafn  14458  imasvscaval  14459  xpsaddlem  14496  xpsvsca  14500  xpsle  14502  comffval  14621  oppccofval  14638  isoval  14686  funcf2  14761  idfu2nd  14770  resf2nd  14788  wunfunc  14792  funcpropd  14793  fucco  14855  homaval  14882  setcco  14934  catcco  14952  xpcco  14976  xpchom2  14979  xpcco2  14980  xpccatid  14981  prfcl  14996  prf1st  14997  prf2nd  14998  catcxpccl  15000  evlf2  15011  curf1cl  15021  curf2cl  15024  curfcl  15025  uncf1  15029  uncf2  15030  uncfcurf  15032  diag11  15036  diag12  15037  diag2  15038  curf2ndf  15040  hof2fval  15048  yonedalem21  15066  yonedalem22  15071  yonedalem3b  15072  yonffthlem  15075  joindmss  15160  meetdmss  15174  latcl2  15201  latlem  15202  latjcom  15212  latmcom  15228  lsmhash  16182  efgmf  16190  efglem  16193  vrgpf  16245  vrgpinv  16246  frgpuplem  16249  frgpup2  16253  frgpnabllem1  16331  mamudi  18149  mamudir  18150  mamuvs1  18151  mamuvs2  18152  mdetrsca  18252  txbas  18982  txcls  19019  txcnp  19035  upxp  19038  txcnmpt  19039  uptx  19040  txlly  19051  txnlly  19052  txtube  19055  txcmplem1  19056  txlm  19063  lmcn2  19064  tx1stc  19065  txkgen  19067  xkococnlem  19074  cnmpt21  19086  txhmeo  19218  txswaphmeolem  19219  txswaphmeo  19220  ptuncnv  19222  txflf  19421  flfcnp2  19422  tmdcn2  19502  clssubg  19521  divstgplem  19533  tsmsadd  19563  imasdsf1olem  19790  xpsdsval  19798  comet  19930  txmetcnp  19964  metustidOLD  19976  metustid  19977  metustsymOLD  19978  metustsym  19979  nrmmetd  20009  isngp3  20032  ngpds  20037  tngnm  20079  qtopbaslem  20179  cnmetdval  20192  remetdval  20208  tgqioo  20219  cnheiborlem  20368  bndth  20372  htpyco2  20393  phtpyco2  20404  bcthlem5  20681  ovollb2lem  20813  ovolctb  20815  ovoliunlem2  20828  ovolscalem1  20838  ovolicc1  20841  ioombl1lem1  20881  ioorf  20895  ioorcl  20899  dyadf  20913  itg1addlem4  21019  limccnp2  21209  dvcnp2  21236  dvaddbr  21254  dvmulbr  21255  dvcobr  21262  dvef  21294  lhop1lem  21327  taylthlem2  21724  dvdsmulf1o  22419  tgelrnln  22907  tghilbert1_1  22914  brcgr  22969  imsdval  23900  sspval  23944  elovimad  25780  ofoprabco  25806  f1od2  25848  prsdm  26198  prsrn  26199  mbfmco2  26534  eulerpartlemgh  26609  afsval  26843  erdszelem9  26935  cvmlift2lem1  27039  cvmlift2lem9  27048  cvmlift2lem10  27049  cvmlift2lem12  27051  cvmlift2lem13  27052  cvmliftphtlem  27054  fvtransport  27910  colinearex  27938  finixpnum  28258  heicant  28270  mblfinlem1  28272  mblfinlem2  28273  ftc1anc  28319  areacirc  28333  opropabco  28461  heiborlem5  28558  fnotaovb  29950  aovmpt4g  29953  el2xptp0  29973  matsubgcell  30641  matvscacell  30642  dvhelvbasei  34306  dvhopvadd  34311  dvhvaddcl  34313  dvhopvsca  34320  dvhvscacl  34321  dvhgrp  34325  dvhopclN  34331  dvhopaddN  34332  dvhopspN  34333  dib1dim2  34386  diblss  34388  diclspsn  34412  dih1dimatlem  34547
  Copyright terms: Public domain W3C validator