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

Theorem opelxpi 5017
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 5015 . 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 1802   <.cop 4016    X. cxp 4983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pr 4672
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-opab 4492  df-xp 4991
This theorem is referenced by:  opelvvg  5031  opelvv  5032  opbrop  5065  fliftrel  6187  elovimad  6318  fnotovb  6319  ov3  6420  ovres  6423  fovrn  6426  fnovrn  6431  ovima0  6435  ovconst2  6436  opabex2  6719  el2xptp0  6825  opiota  6840  oprab2co  6866  1stconst  6869  2ndconst  6870  fnwelem  6896  seqomlem2  7114  brdifun  7336  ecopqsi  7366  brecop  7402  eceqoveq  7414  xpcomco  7605  xpf1o  7677  xpmapenlem  7682  unxpdomlem3  7724  fseqenlem1  8403  fseqenlem2  8404  isfin4-3  8693  axdc4lem  8833  iundom2g  8913  canthp1lem2  9029  addpiord  9260  mulpiord  9261  pinq  9303  nqereu  9305  addpipq  9313  addpqnq  9314  mulpipq  9316  mulpqnq  9317  ordpipq  9318  addpqf  9320  mulpqf  9322  recmulnq  9340  dmrecnq  9344  ltexnq  9351  enreceq  9441  addsrpr  9450  mulsrpr  9451  0r  9455  1sr  9456  m1r  9457  addclsr  9458  mulclsr  9459  axaddf  9520  axmulf  9521  xrlenlt  9650  uzrdgfni  12043  swrdval  12618  cnrecnv  12972  ruclem1  13836  ruclem6  13840  eucalgf  14084  eucalg  14088  qredeu  14120  qnumdenbi  14149  crt  14180  phimullem  14181  prmreclem3  14308  setscom  14534  strfv2d  14536  setsid  14545  imasaddfnlem  14797  imasaddflem  14799  imasvscafn  14806  imasvscaval  14807  xpsaddlem  14844  xpsvsca  14848  xpsle  14850  comffval  14966  oppccofval  14983  isoval  15031  funcf2  15106  idfu2nd  15115  resf2nd  15133  wunfunc  15137  funcpropd  15138  fucco  15200  homaval  15227  setcco  15279  catcco  15297  xpcco  15321  xpchom2  15324  xpcco2  15325  xpccatid  15326  prfcl  15341  prf1st  15342  prf2nd  15343  catcxpccl  15345  evlf2  15356  curf1cl  15366  curf2cl  15369  curfcl  15370  uncf1  15374  uncf2  15375  uncfcurf  15377  diag11  15381  diag12  15382  diag2  15383  curf2ndf  15385  hof2fval  15393  yonedalem21  15411  yonedalem22  15416  yonedalem3b  15417  yonffthlem  15420  joindmss  15506  meetdmss  15520  latcl2  15547  latlem  15548  latjcom  15558  latmcom  15574  lsmhash  16592  efgmf  16600  efglem  16603  vrgpf  16655  vrgpinv  16656  frgpuplem  16659  frgpup2  16663  frgpnabllem1  16746  mamudi  18772  mamudir  18773  mamuvs1  18774  mamuvs2  18775  matsubgcell  18803  matvscacell  18805  mdetrsca  18972  pmatcoe1fsupp  19069  txbas  19934  txcls  19971  txcnp  19987  upxp  19990  txcnmpt  19991  uptx  19992  txlly  20003  txnlly  20004  txtube  20007  txcmplem1  20008  txlm  20015  lmcn2  20016  tx1stc  20017  txkgen  20019  xkococnlem  20026  cnmpt21  20038  txhmeo  20170  txswaphmeolem  20171  txswaphmeo  20172  ptuncnv  20174  txflf  20373  flfcnp2  20374  tmdcn2  20454  clssubg  20473  qustgplem  20485  tsmsadd  20515  imasdsf1olem  20742  xpsdsval  20750  comet  20882  txmetcnp  20916  metustidOLD  20928  metustid  20929  metustsymOLD  20930  metustsym  20931  nrmmetd  20961  isngp3  20984  ngpds  20989  tngnm  21031  qtopbaslem  21131  cnmetdval  21144  remetdval  21160  tgqioo  21171  cnheiborlem  21320  bndth  21324  htpyco2  21345  phtpyco2  21356  bcthlem5  21633  ovollb2lem  21765  ovolctb  21767  ovoliunlem2  21780  ovolscalem1  21790  ovolicc1  21793  ioombl1lem1  21834  ioorf  21848  ioorcl  21852  dyadf  21866  itg1addlem4  21972  limccnp2  22162  dvcnp2  22189  dvaddbr  22207  dvmulbr  22208  dvcobr  22215  dvef  22247  lhop1lem  22280  taylthlem2  22634  dvdsmulf1o  23335  tgelrnln  23875  brcgr  24068  imsdval  25457  sspval  25501  ofoprabco  27370  f1od2  27412  fimaproj  27702  qtophaus  27705  prsdm  27762  prsrn  27763  mbfmco2  28102  eulerpartlemgh  28183  afsval  28417  erdszelem9  28509  cvmlift2lem1  28613  cvmlift2lem9  28622  cvmlift2lem10  28623  cvmlift2lem12  28625  cvmlift2lem13  28626  cvmliftphtlem  28628  msubco  28757  msubff1  28782  mvhf  28784  msubvrs  28786  fvtransport  29650  colinearex  29678  finixpnum  30006  heicant  30017  mblfinlem1  30019  mblfinlem2  30020  ftc1anc  30066  areacirc  30080  opropabco  30182  heiborlem5  30279  fnotaovb  32117  aovmpt4g  32120  estrcco  32475  rngccoOLD  32515  ringccoOLD  32571  rhmsubclem2  32603  rhmsubcOLDlem2  32622  dvhelvbasei  36517  dvhopvadd  36522  dvhvaddcl  36524  dvhopvsca  36531  dvhvscacl  36532  dvhgrp  36536  dvhopclN  36542  dvhopaddN  36543  dvhopspN  36544  dib1dim2  36597  diblss  36599  diclspsn  36623  dih1dimatlem  36758
  Copyright terms: Public domain W3C validator