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

Definition df-br 4410
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 often denotes a relation such as " " that compares two classes and , which might be numbers such as and (see df-ltxr 9560 for the specific definition of ). As a wff, relations are true or false. For example, (ex-br 24107). Often class meets the Rel criteria to be defined in df-rel 4964, and in particular may be a function (see df-fun 5539). This definition of relations is well-defined, although not very meaningful, when classes and/or are proper classes (i.e. are not sets). On the other hand, we often find uses for this definition when is a proper class (see for example iprc 6646). (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
df-br

Detailed syntax breakdown of Definition df-br
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cR . . 3
41, 2, 3wbr 4409 . 2
51, 2cop 3999 . . 3
65, 3wcel 1758 . 2
74, 6wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  breq  4411  breq1  4412  breq2  4413  ssbrd  4450  nfbrd  4452  br0  4455  brne0  4456  brun  4457  brin  4458  brdif  4459  sbcbr123  4460  opabss  4470  brabsb  4717  brabga  4720  epelg  4750  pofun  4774  brxp  4987  brab2a  5005  brab2ga  5029  eqbrriv  5052  eqbrrdv  5054  eqbrrdiv  5055  opeliunxp2  5095  opelco2g  5124  opelco  5128  cnvss  5129  elcnv2  5134  opelcnvg  5136  brcnvg  5137  dfdm3  5144  dfrn3  5146  elrng  5148  eldm2g  5153  breldm  5161  dmopab  5167  opelrn  5188  elrn  5197  rnopab  5201  brres  5234  brresg  5236  resieq  5238  opelresi  5239  iss  5272  dfres2  5277  restidsing  5281  dfima3  5291  elima3  5295  imai  5300  elimasn  5313  elimasni  5315  eliniseg  5317  cotr  5329  issref  5330  cnvsym  5331  intasym  5332  asymref  5333  asymref2  5334  intirr  5335  codir  5337  qfto  5338  poirr2  5341  xpdifid  5385  sofld  5405  dmsnn0  5423  coiun  5466  co02  5470  coi1  5472  dffun4  5549  dffun5  5550  funeu2  5562  funopab  5570  funcnvsn  5582  isarep1  5616  fnop  5633  fneu2  5635  brprcneu  5806  dffv3  5809  tz6.12  5830  funopfv  5854  fnopfvb  5856  opabiota  5877  dffv2  5887  fvopab5  5918  funfvbrb  5939  dff3  5979  dff4  5980  f1ompt  5988  idref  6083  foeqcnvco  6129  f1eqcocnv  6130  fliftel  6133  fliftel1  6134  fliftcnv  6135  f1oiso  6173  ovprc  6249  brabv  6264  elrnmpt2res  6337  resiexg  6647  1st2ndbr  6756  bropopvvv  6786  frxp  6816  xporderlem  6817  cnvimadfsn  6833  brovex  6874  isprmpt2  6877  ottpos  6889  dftpos3  6897  dftpos4  6898  tposoprab  6915  tfrlem7  6976  tfrlem9a  6979  seqomlem2  7040  seqomlem3  7041  seqomlem4  7042  0we1  7080  brwitnlem  7081  ercnv  7256  brdifun  7262  swoord1  7264  swoord2  7265  0er  7270  elecg  7273  iiner  7306  brecop  7327  brsdom  7466  brdom2  7473  idssen  7488  xpcomco  7535  omxpenlem  7546  brsdom2  7569  infxpenlem  8317  dcomex  8753  brdom3  8832  brdom7disj  8835  brdom6disj  8836  fpwwe2lem8  8941  fpwwe2lem9  8942  fpwwe2lem12  8945  canthwe  8955  dmrecnq  9274  xrlenlt  9579  climcau  13306  caucvgb  13315  divides  13695  vdwpc  14199  isstruct  14342  prdsleval  14574  imasaddfnlem  14625  imasvscafn  14634  invsym2  14860  funcf1  14935  funcixp  14936  funcid  14939  funcco  14940  funcsect  14941  funcinv  14942  funciso  14943  funcoppc  14944  idfucl  14950  cofuval2  14956  cofucl  14957  funcres  14965  funcres2b  14966  funcres2  14967  wunfunc  14968  funcpropd  14969  funcres2c  14970  isfull  14979  isfth  14983  fthsect  14994  fthinv  14995  fthmon  14996  fthepi  14997  ffthiso  14998  fthres2  15001  idffth  15002  cofull  15003  cofth  15004  ressffth  15007  isnat  15016  natixp  15021  nati  15024  elhomai2  15061  homa1  15064  homahom2  15065  eldmcoa  15092  coapm  15098  catcisolem  15133  catciso  15134  1stfcl  15166  2ndfcl  15167  prfcl  15172  evlfcl  15191  curf1cl  15197  curfcl  15201  hofcl  15228  yonedalem1  15241  yonedalem21  15242  yonedalem22  15247  yonffthlem  15251  yoniso  15254  pospo  15302  efgi  16377  efgi2  16383  gsum2d2lem  16634  dmdprd  16655  dprdval  16660  eldprd  16661  dprdvalOLD  16662  eldprdOLD  16663  dprd2dlem2  16714  dprd2dlem1  16715  dprd2da  16716  dprd2d2  16718  isunit  16925  subrgdvds  17055  opsrtoslem2  17743  eltopspOLD  18922  tpsexOLD  18923  lmrcl  19234  lmff  19304  2ndcctbss  19458  2ndcdisj  19459  hausdiag  19617  hauseqlcld  19618  cnextfun  20035  cnextfvval  20036  tgphaus  20086  utop2nei  20224  utop3cls  20225  ucnima  20255  xmeterval  20406  metustidOLD  20533  metustid  20534  metustsymOLD  20535  metustsym  20536  metustexhalfOLD  20537  metustexhalf  20538  elbl4  20550  metuel2  20553  isphtpc  20965  ovolfcl  21349  ovollb2lem  21370  ovolctb  21372  ovolshftlem1  21391  ovolscalem1  21395  ovolicc1  21398  ioombl1lem1  21439  ioorf  21453  dyadf  21471  eldv  21773  dvres2  21787  dvef  21852  eltayl  22225  ulmscl  22244  tglngne  23401  tgelrnln  23460  tghilbert1_1  23467  isperp  23533  brbtwn  23614  iswlk  23895  istrl  23905  ispth  23936  isspth  23937  ex-br  24107  avril1  24125  helloworld  24127  isrngo  24334  rngoablo2  24378  isdivrngo  24387  vcex  24427  h2hlm  24851  axhcompl-zf  24869  opabdm  26411  opabrn  26412  fpwrelmap  26500  isarchi  26660  gsummpt2co  26706  prsdm  26801  prsrn  26802  relexpindlem  27797  dfrtrclrec2  27801  rtrclreclem.trans  27804  brtpid1  27833  brtpid2  27834  brtpid3  27835  brtp  28015  dfso2  28020  dfpo2  28021  fundmpss  28033  opelco3  28045  elpredim  28093  elpredg  28095  wfrlem11  28190  frrlem5c  28230  brsymdif  28315  brv  28364  pprodss4v  28371  brsset  28376  brtxpsd  28381  sscoid  28400  dffun10  28401  brimg  28424  funpartfun  28430  funpartfv  28432  dfrdg4  28437  imagesset  28440  fvtransport  28519  brcolinear2  28545  colineardim1  28548  fvray  28628  fvline  28631  mblfinlem2  28889  areacirclem5  28948  eltail  29055  heiborlem3  29172  heiborlem4  29173  heiborlem6  29175  brabsb2  29467  eqbrrdv2  29468  fourierdlem42  30678  afveu  30936  fnopafvb  30938  tz6.12-afv  30956  tz6.12-1-afv  30957  aovprc  30971  aovrcl  30972  oprabv  31034  wlkcomp  31163  2wlkeq  31165  wlkcpr  31167  wlknwwlknsur  31221  wlkiswwlksur  31228  isclwlk0  31296  clwlkswlks  31300  clwlkcomp  31303  wlkp1lenfislenp  31389  clwlkfoclwwlk  31395  isrgra  31420  isrusgra  31421  cmtvalN  33707  cvrval  33765  cotrgen  36473
  Copyright terms: Public domain W3C validator