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

Theorem opelxpi 5036
Description: Ordered pair membership in a Cartesian product (implication). (Contributed by NM, 28-May-1995.)
Assertion
Ref Expression
opelxpi

Proof of Theorem opelxpi
StepHypRef Expression
1 opelxp 5034 . 2
21biimpri 206 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  <.cop 4035  X.cxp 5002
This theorem is referenced by:  opelvvg  5050  opelvv  5051  opbrop  5084  fliftrel  6206  elovimad  6337  fnotovb  6338  ov3  6439  ovres  6442  fovrn  6445  fnovrn  6450  ovima0  6454  ovconst2  6455  opabex2  6738  el2xptp0  6844  opiota  6859  oprab2co  6885  1stconst  6888  2ndconst  6889  fnwelem  6915  seqomlem2  7135  brdifun  7357  ecopqsi  7387  brecop  7423  eceqoveq  7435  xpcomco  7627  xpf1o  7699  xpmapenlem  7704  unxpdomlem3  7746  fseqenlem1  8426  fseqenlem2  8427  isfin4-3  8716  axdc4lem  8856  iundom2g  8936  canthp1lem2  9052  addpiord  9283  mulpiord  9284  pinq  9326  nqereu  9328  addpipq  9336  addpqnq  9337  mulpipq  9339  mulpqnq  9340  ordpipq  9341  addpqf  9343  mulpqf  9345  recmulnq  9363  dmrecnq  9367  ltexnq  9374  enreceq  9464  addsrpr  9473  mulsrpr  9474  0r  9478  1sr  9479  m1r  9480  addclsr  9481  mulclsr  9482  axaddf  9543  axmulf  9544  xrlenlt  9673  uzrdgfni  12069  swrdval  12644  cnrecnv  12998  ruclem1  13964  ruclem6  13968  eucalgf  14212  eucalg  14216  qredeu  14248  qnumdenbi  14277  crt  14308  phimullem  14309  prmreclem3  14436  setscom  14662  strfv2d  14664  setsid  14673  imasaddfnlem  14925  imasaddflem  14927  imasvscafn  14934  imasvscaval  14935  xpsaddlem  14972  xpsvsca  14976  xpsle  14978  comffval  15094  oppccofval  15111  isoval  15159  funcf2  15237  idfu2nd  15246  resf2nd  15264  wunfunc  15268  funcpropd  15269  fucco  15331  homaval  15358  setcco  15410  catcco  15428  xpcco  15452  xpchom2  15455  xpcco2  15456  xpccatid  15457  prfcl  15472  prf1st  15473  prf2nd  15474  catcxpccl  15476  evlf2  15487  curf1cl  15497  curf2cl  15500  curfcl  15501  uncf1  15505  uncf2  15506  uncfcurf  15508  diag11  15512  diag12  15513  diag2  15514  curf2ndf  15516  hof2fval  15524  yonedalem21  15542  yonedalem22  15547  yonedalem3b  15548  yonffthlem  15551  joindmss  15637  meetdmss  15651  latcl2  15678  latlem  15679  latjcom  15689  latmcom  15705  lsmhash  16723  efgmf  16731  efglem  16734  vrgpf  16786  vrgpinv  16787  frgpuplem  16790  frgpup2  16794  frgpnabllem1  16877  mamudi  18905  mamudir  18906  mamuvs1  18907  mamuvs2  18908  matsubgcell  18936  matvscacell  18938  mdetrsca  19105  pmatcoe1fsupp  19202  txbas  20068  txcls  20105  txcnp  20121  upxp  20124  txcnmpt  20125  uptx  20126  txlly  20137  txnlly  20138  txtube  20141  txcmplem1  20142  txlm  20149  lmcn2  20150  tx1stc  20151  txkgen  20153  xkococnlem  20160  cnmpt21  20172  txhmeo  20304  txswaphmeolem  20305  txswaphmeo  20306  ptuncnv  20308  txflf  20507  flfcnp2  20508  tmdcn2  20588  clssubg  20607  qustgplem  20619  tsmsadd  20649  imasdsf1olem  20876  xpsdsval  20884  comet  21016  txmetcnp  21050  metustidOLD  21062  metustid  21063  metustsymOLD  21064  metustsym  21065  nrmmetd  21095  isngp3  21118  ngpds  21123  tngnm  21165  qtopbaslem  21265  cnmetdval  21278  remetdval  21294  tgqioo  21305  cnheiborlem  21454  bndth  21458  htpyco2  21479  phtpyco2  21490  bcthlem5  21767  ovollb2lem  21899  ovolctb  21901  ovoliunlem2  21914  ovolscalem1  21924  ovolicc1  21927  ioombl1lem1  21968  ioorf  21982  ioorcl  21986  dyadf  22000  itg1addlem4  22106  limccnp2  22296  dvcnp2  22323  dvaddbr  22341  dvmulbr  22342  dvcobr  22349  dvef  22381  lhop1lem  22414  taylthlem2  22769  dvdsmulf1o  23470  tgelrnln  24010  brcgr  24203  imsdval  25592  sspval  25636  ofoprabco  27505  f1od2  27547  fimaproj  27836  qtophaus  27839  prsdm  27896  prsrn  27897  mbfmco2  28236  eulerpartlemgh  28317  afsval  28551  erdszelem9  28643  cvmlift2lem1  28747  cvmlift2lem9  28756  cvmlift2lem10  28757  cvmlift2lem12  28759  cvmlift2lem13  28760  cvmliftphtlem  28762  msubco  28891  msubff1  28916  mvhf  28918  msubvrs  28920  fvtransport  29682  colinearex  29710  finixpnum  30038  heicant  30049  mblfinlem1  30051  mblfinlem2  30052  ftc1anc  30098  areacirc  30112  opropabco  30214  heiborlem5  30311  fnotaovb  32283  aovmpt4g  32286  estrcco  32636  rngccoOLD  32796  ringccoOLD  32859  rhmsubclem2  32895  rhmsubcOLDlem2  32914  dvhelvbasei  36815  dvhopvadd  36820  dvhvaddcl  36822  dvhopvsca  36829  dvhvscacl  36830  dvhgrp  36834  dvhopclN  36840  dvhopaddN  36841  dvhopspN  36842  dib1dim2  36895  diblss  36897  diclspsn  36921  dih1dimatlem  37056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-opab 4511  df-xp 5010
  Copyright terms: Public domain W3C validator