MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-br Structured version   Visualization version   Unicode version

Definition df-br 4417
Description: Define a general binary relation. Note that the syntax is simply three class symbols in a row. Definition 6.18 of [TakeutiZaring] p. 29 generalized to arbitrary classes. Class  R often denotes a relation such as " < " that compares two classes  A and 
B, which might be numbers such as  1 and  2 (see df-ltxr 9706 for the specific definition of  <). As a wff, relations are true or false. For example,  ( R  =  { <. 2 ,  6
>. ,  <. 3 ,  9 >. }  ->  3 R 9 ) (ex-br 25930). Often class  R meets the  Rel criteria to be defined in df-rel 4860, and in particular  R may be a function (see df-fun 5603). This definition of relations is well-defined, although not very meaningful, when classes  A and/or  B are proper classes (i.e. are not sets). On the other hand, we often find uses for this definition when  R is a proper class (see for example iprc 6755). (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
df-br  |-  ( A R B  <->  <. A ,  B >.  e.  R )

Detailed syntax breakdown of Definition df-br
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cR . . 3  class  R
41, 2, 3wbr 4416 . 2  wff  A R B
51, 2cop 3986 . . 3  class  <. A ,  B >.
65, 3wcel 1898 . 2  wff  <. A ,  B >.  e.  R
74, 6wb 189 1  wff  ( A R B  <->  <. A ,  B >.  e.  R )
Colors of variables: wff setvar class
This definition is referenced by:  breq  4418  breq1  4419  breq2  4420  ssbrd  4458  nfbrd  4460  br0  4463  brne0  4464  brun  4465  brin  4466  brdif  4467  brsymdif  4473  opabss  4478  brabsb  4726  brabga  4729  elopabr  4752  rbropapd  4754  epelg  4765  pofun  4790  brxp  4884  brab2a  4903  bropaex12  4927  brab2ga  4929  eqbrriv  4949  eqbrrdv  4951  eqbrrdiv  4952  opeliunxp2  4992  opelco2g  5021  opelco  5025  cnvss  5026  elcnv2  5031  opelcnvg  5033  brcnvg  5034  dfdm3  5041  dfrn3  5043  elrng  5045  eldm2g  5050  breldm  5058  dmopab  5064  opelrn  5085  elrn  5094  rnopab  5098  brres  5130  brresg  5132  resieq  5134  opelresi  5135  iss  5171  dfres2  5176  restidsing  5180  dfima3  5190  elima3  5194  imai  5199  elimasn  5212  elimasni  5214  eliniseg  5216  cotrg  5230  issref  5232  cnvsym  5233  intasym  5234  asymref  5235  asymref2  5236  intirr  5237  codir  5239  qfto  5240  poirr2  5243  xpdifid  5284  sofld  5303  dmsnn0  5320  coiun  5364  coi1  5370  elpredim  5411  elpredg  5413  dffun4  5613  dffun5  5614  funeu2  5626  funopab  5634  funcnvsn  5646  isarep1  5684  fnop  5701  fneu2  5703  brprcneu  5881  dffv3  5884  tz6.12  5905  funopfv  5927  fnopfvb  5929  opabiota  5951  dffv2  5961  fvopab5  5997  funfvbrb  6018  dff3  6058  dff4  6059  f1ompt  6067  idref  6171  foeqcnvco  6223  f1eqcocnv  6224  fliftel  6227  fliftel1  6228  fliftcnv  6229  f1oiso  6267  ovprc  6345  brabv  6362  oprabv  6366  elrnmpt2res  6437  resiexg  6756  1st2ndbr  6869  brovpreldm  6900  bropopvvv  6901  frxp  6933  xporderlem  6934  cnvimadfsn  6950  opeliunxp2f  6983  brovex  6995  ottpos  7009  dftpos3  7017  dftpos4  7018  tposoprab  7035  wfrfun  7072  wfrlem17  7078  tfrlem7  7127  tfrlem9a  7130  seqomlem2  7194  seqomlem3  7195  seqomlem4  7196  brwitnlem  7235  ercnv  7410  brdifun  7416  swoord1  7418  swoord2  7419  0er  7424  elecg  7428  iiner  7461  brecop  7482  brsdom  7618  brdom2  7625  idssen  7640  xpcomco  7688  omxpenlem  7699  brsdom2  7722  infxpenlem  8470  dcomex  8903  brdom7disj  8985  brdom6disj  8986  fpwwe2lem8  9088  fpwwe2lem9  9089  fpwwe2lem12  9092  dmrecnq  9419  xrlenlt  9725  brintclab  13114  brtrclfv  13115  dfrtrclrec2  13169  rtrclreclem3  13172  relexpindlem  13175  climcau  13783  caucvgb  13795  divides  14356  vdwpc  14979  isstruct  15180  prdsleval  15424  imasaddfnlem  15483  imasvscafn  15492  invsym2  15717  brcic  15752  ciclcl  15756  cicrcl  15757  cicsym  15758  funcf1  15820  funcixp  15821  funcid  15824  funcco  15825  funcsect  15826  funcinv  15827  funciso  15828  funcoppc  15829  idfucl  15835  cofuval2  15841  cofucl  15842  funcres  15850  funcres2b  15851  funcres2  15852  wunfunc  15853  funcpropd  15854  funcres2c  15855  isfull  15864  isfth  15868  fthsect  15879  fthinv  15880  fthmon  15881  fthepi  15882  ffthiso  15883  fthres2  15886  idffth  15887  cofull  15888  cofth  15889  ressffth  15892  isnat  15901  natixp  15906  nati  15909  elhomai2  15978  homa1  15981  homahom2  15982  eldmcoa  16009  coapm  16015  catcisolem  16050  catciso  16051  1stfcl  16131  2ndfcl  16132  prfcl  16137  evlfcl  16156  curf1cl  16162  curfcl  16166  hofcl  16193  yonedalem1  16206  yonedalem21  16207  yonedalem22  16212  yonffthlem  16216  yoniso  16219  pospo  16268  efgi  17418  efgi2  17424  gsum2d2lem  17654  dmdprd  17679  dprdval  17684  eldprd  17685  dprd2dlem2  17722  dprd2dlem1  17723  dprd2da  17724  dprd2d2  17726  isunit  17934  subrgdvds  18071  opsrtoslem2  18757  lmrcl  20296  lmff  20366  2ndcctbss  20519  2ndcdisj  20520  hausdiag  20709  hauseqlcld  20710  cnextfun  21128  cnextfvval  21129  cnextfres  21133  tgphaus  21180  utop2nei  21314  utop3cls  21315  ucnima  21345  xmeterval  21496  metustid  21618  metustsym  21619  metustexhalf  21620  elbl4  21627  metuel2  21629  isphtpc  22074  ovolfcl  22468  ovollb2lem  22490  ovolctb  22492  ovolshftlem1  22511  ovolscalem1  22515  ovolicc1  22518  ioombl1lem1  22560  ioorf  22574  ioorfOLD  22579  dyadf  22598  eldv  22902  dvres2  22916  dvef  22981  eltayl  23364  ulmscl  23383  tglngne  24644  tgelrnln  24724  isperp  24806  brbtwn  24978  uhgraop  25080  usgrac  25127  elusuhgra  25144  usgraexmplc  25181  iswlk  25297  wlkcomp  25302  wlkcpr  25306  istrl  25316  ispth  25347  isspth  25348  2wlkeq  25484  wlknwwlknsur  25489  wlkiswwlksur  25496  isclwlk0  25531  clwlkswlks  25535  clwlkcomp  25540  wlklenvclwlk  25616  clwlkfoclwwlk  25622  isrgra  25703  isrusgra  25704  isrusgusrgcl  25710  0eusgraiff0rgracl  25718  ex-br  25930  avril1  25949  helloworld  25951  isrngo  26155  rngoablo2  26199  isdivrngo  26208  vcex  26248  h2hlm  26682  axhcompl-zf  26700  opeldifid  28259  brabgaf  28265  opabdm  28268  opabrn  28269  fpwrelmap  28367  isarchi  28548  gsummpt2co  28592  qtophaus  28712  prsdm  28769  prsrn  28770  mclsax  30256  brtpid1  30402  brtpid2  30403  brtpid3  30404  brtp  30438  dfso2  30443  dfpo2  30444  fundmpss  30456  opelco3  30469  frrlem5c  30569  brv  30693  pprodss4v  30700  brsset  30705  brtxpsd  30710  sscoid  30729  dffun10  30730  brimg  30753  funpartfun  30759  funpartfv  30761  dfrecs2  30766  dfrdg4  30767  imagesset  30769  fvtransport  30848  brcolinear2  30874  colineardim1  30877  fvray  30957  fvline  30960  eltail  31079  phpreu  31974  poimirlem26  32011  mblfinlem2  32023  areacirclem5  32081  heiborlem3  32190  heiborlem4  32191  heiborlem6  32193  brabsb2  32479  eqbrrdv2  32480  cmtvalN  32822  cvrval  32880  undmrnresiss  36255  cnvssco  36257  cotrintab  36266  elimaint  36285  coiun1  36289  elintima  36290  briunov2  36319  brtrclfv2  36364  frege77d  36383  dfhe3  36415  dffrege76  36580  frege97  36601  frege98  36602  frege109  36613  frege110  36614  dffrege115  36619  frege131  36635  frege133  36637  fourierdlem42  38050  fourierdlem42OLD  38051  afveu  38693  fnopafvb  38695  tz6.12-afv  38713  tz6.12-1-afv  38714  aovprc  38728  aovrcl  38729  is1wlk  39676  isWlk  39677  1wlkcpr  39691  1wlkcomp  39692  clWlkcomp  39805  uhgrasiz  39979  isfusgracl  40011  isfusgraclALT  40013  fusgraimpclALT2  40016  usgrafisbaseALT  40025  usgrafisbaseALT2  40026  usgfis  40031  usgfisALT  40035  inclfusubc  40140  funcrngcsetc  40273  funcrngcsetcALT  40274  funcringcsetc  40310
  Copyright terms: Public domain W3C validator