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

Definition df-br 4438
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 9636 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 25130). Often class  R meets the  Rel criteria to be defined in df-rel 4996, and in particular  R may be a function (see df-fun 5580). 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 6720). (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 4437 . 2  wff  A R B
51, 2cop 4020 . . 3  class  <. A ,  B >.
65, 3wcel 1804 . 2  wff  <. A ,  B >.  e.  R
74, 6wb 184 1  wff  ( A R B  <->  <. A ,  B >.  e.  R )
Colors of variables: wff setvar class
This definition is referenced by:  breq  4439  breq1  4440  breq2  4441  ssbrd  4478  nfbrd  4480  br0  4483  brne0  4484  brun  4485  brin  4486  brdif  4487  opabss  4498  brabsb  4748  brabga  4751  epelg  4782  pofun  4806  brxp  5020  brab2a  5039  bropaex12  5063  brab2ga  5065  eqbrriv  5088  eqbrrdv  5090  eqbrrdiv  5091  opeliunxp2  5131  opelco2g  5160  opelco  5164  cnvss  5165  elcnv2  5170  opelcnvg  5172  brcnvg  5173  dfdm3  5180  dfrn3  5182  elrng  5184  eldm2g  5189  breldm  5197  dmopab  5203  opelrn  5224  elrn  5233  rnopab  5237  brres  5270  brresg  5272  resieq  5274  opelresi  5275  iss  5311  dfres2  5316  restidsing  5320  dfima3  5330  elima3  5334  imai  5339  elimasn  5352  elimasni  5354  eliniseg  5356  cotrg  5368  issref  5370  cnvsym  5371  intasym  5372  asymref  5373  asymref2  5374  intirr  5375  codir  5377  qfto  5378  poirr2  5381  xpdifid  5425  sofld  5445  dmsnn0  5463  coiun  5507  coi1  5513  dffun4  5590  dffun5  5591  funeu2  5603  funopab  5611  funcnvsn  5623  isarep1  5657  fnop  5674  fneu2  5676  brprcneu  5849  dffv3  5852  tz6.12  5873  funopfv  5897  fnopfvb  5899  opabiota  5921  dffv2  5931  fvopab5  5964  funfvbrb  5985  dff3  6029  dff4  6030  f1ompt  6038  idref  6138  foeqcnvco  6188  f1eqcocnv  6189  fliftel  6192  fliftel1  6193  fliftcnv  6194  f1oiso  6232  ovprc  6311  brabv  6327  oprabv  6330  elrnmpt2res  6401  resiexg  6721  1st2ndbr  6834  bropopvvv  6865  frxp  6895  xporderlem  6896  cnvimadfsn  6912  brovex  6952  isprmpt2  6955  ottpos  6967  dftpos3  6975  dftpos4  6976  tposoprab  6993  tfrlem7  7054  tfrlem9a  7057  seqomlem2  7118  seqomlem3  7119  seqomlem4  7120  brwitnlem  7159  ercnv  7334  brdifun  7340  swoord1  7342  swoord2  7343  0er  7348  elecg  7352  iiner  7385  brecop  7406  brsdom  7540  brdom2  7547  idssen  7562  xpcomco  7609  omxpenlem  7620  brsdom2  7643  infxpenlem  8394  dcomex  8830  brdom7disj  8912  brdom6disj  8913  fpwwe2lem8  9018  fpwwe2lem9  9019  fpwwe2lem12  9022  dmrecnq  9349  xrlenlt  9655  climcau  13475  caucvgb  13484  divides  13970  vdwpc  14480  isstruct  14624  prdsleval  14856  imasaddfnlem  14907  imasvscafn  14916  invsym2  15139  funcf1  15214  funcixp  15215  funcid  15218  funcco  15219  funcsect  15220  funcinv  15221  funciso  15222  funcoppc  15223  idfucl  15229  cofuval2  15235  cofucl  15236  funcres  15244  funcres2b  15245  funcres2  15246  wunfunc  15247  funcpropd  15248  funcres2c  15249  isfull  15258  isfth  15262  fthsect  15273  fthinv  15274  fthmon  15275  fthepi  15276  ffthiso  15277  fthres2  15280  idffth  15281  cofull  15282  cofth  15283  ressffth  15286  isnat  15295  natixp  15300  nati  15303  elhomai2  15340  homa1  15343  homahom2  15344  eldmcoa  15371  coapm  15377  catcisolem  15412  catciso  15413  1stfcl  15445  2ndfcl  15446  prfcl  15451  evlfcl  15470  curf1cl  15476  curfcl  15480  hofcl  15507  yonedalem1  15520  yonedalem21  15521  yonedalem22  15526  yonffthlem  15530  yoniso  15533  pospo  15582  efgi  16716  efgi2  16722  gsum2d2lem  16980  dmdprd  17008  dprdval  17013  eldprd  17014  dprdvalOLD  17015  eldprdOLD  17016  dprd2dlem2  17068  dprd2dlem1  17069  dprd2da  17070  dprd2d2  17072  isunit  17285  subrgdvds  17422  opsrtoslem2  18128  eltopspOLD  19397  tpsexOLD  19398  lmrcl  19710  lmff  19780  2ndcctbss  19934  2ndcdisj  19935  hausdiag  20124  hauseqlcld  20125  cnextfun  20542  cnextfvval  20543  tgphaus  20593  utop2nei  20731  utop3cls  20732  ucnima  20762  xmeterval  20913  metustidOLD  21040  metustid  21041  metustsymOLD  21042  metustsym  21043  metustexhalfOLD  21044  metustexhalf  21045  elbl4  21057  metuel2  21060  isphtpc  21472  ovolfcl  21856  ovollb2lem  21877  ovolctb  21879  ovolshftlem1  21898  ovolscalem1  21902  ovolicc1  21905  ioombl1lem1  21946  ioorf  21960  dyadf  21978  eldv  22280  dvres2  22294  dvef  22359  eltayl  22733  ulmscl  22752  tglngne  23915  tgelrnln  23988  isperp  24067  brbtwn  24180  uhgraop  24282  usgrac  24329  elusuhgra  24346  usgraexmplc  24382  iswlk  24498  wlkcomp  24503  wlkcpr  24507  istrl  24517  ispth  24548  isspth  24549  2wlkeq  24685  wlknwwlknsur  24690  wlkiswwlksur  24697  isclwlk0  24732  clwlkswlks  24736  clwlkcomp  24741  wlklenvclwlk  24817  clwlkfoclwwlk  24823  isrgra  24904  isrusgra  24905  isrusgusrgcl  24911  0eusgraiff0rgracl  24919  ex-br  25130  avril1  25149  helloworld  25151  isrngo  25358  rngoablo2  25402  isdivrngo  25411  vcex  25451  h2hlm  25875  axhcompl-zf  25893  opeldifid  27434  opabdm  27442  opabrn  27443  fpwrelmap  27534  isarchi  27704  gsummpt2co  27749  qtophaus  27817  prsdm  27874  prsrn  27875  mclsax  28907  relexpindlem  29040  dfrtrclrec2  29044  rtrclreclem.trans  29047  brtpid1  29076  brtpid2  29077  brtpid3  29078  brtp  29154  dfso2  29159  dfpo2  29160  fundmpss  29172  opelco3  29184  elpredim  29232  elpredg  29234  wfrlem11  29329  frrlem5c  29369  brsymdif  29454  brv  29503  pprodss4v  29510  brsset  29515  brtxpsd  29520  sscoid  29539  dffun10  29540  brimg  29563  funpartfun  29569  funpartfv  29571  dfrdg4  29576  imagesset  29579  fvtransport  29658  brcolinear2  29684  colineardim1  29687  fvray  29767  fvline  29770  mblfinlem2  30028  areacirclem5  30087  eltail  30168  heiborlem3  30285  heiborlem4  30286  heiborlem6  30288  brabsb2  30579  eqbrrdv2  30580  fourierdlem42  31885  afveu  32192  fnopafvb  32194  tz6.12-afv  32212  tz6.12-1-afv  32213  aovprc  32227  aovrcl  32228  uhgrasiz  32348  isfusgracl  32380  isfusgraclALT  32382  fusgraimpclALT2  32385  usgrafisbaseALT  32394  usgrafisbaseALT2  32395  usgfis  32400  usgfisALT  32404  inclfusubc  32517  funcrngcsetc  32681  funcrngcsetcALT  32682  funcringcsetc  32715  cmtvalN  34811  cvrval  34869  dfhe3  37621
  Copyright terms: Public domain W3C validator