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

Definition df-br 4375
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 9508 for the specific definition of ). As a wff, relations are true or false. For example, (ex-br 23757). Often class meets the Rel criteria to be defined in df-rel 4929, and in particular may be a function (see df-fun 5502). 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 6597). (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 4374 . 2
51, 2cop 3965 . . 3
65, 3wcel 1757 . 2
74, 6wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  breq  4376  breq1  4377  breq2  4378  ssbrd  4415  nfbrd  4417  br0  4420  brne0  4421  brun  4422  brin  4423  brdif  4424  sbcbr123  4425  opabss  4435  brabsb  4682  brabga  4685  epelg  4715  pofun  4739  brxp  4952  brab2a  4970  brab2ga  4994  eqbrriv  5017  eqbrrdv  5019  eqbrrdiv  5020  opeliunxp2  5060  opelco2g  5089  opelco  5093  cnvss  5094  elcnv2  5099  opelcnvg  5101  brcnvg  5102  dfdm3  5109  dfrn3  5111  elrng  5113  eldm2g  5118  breldm  5126  dmopab  5132  opelrn  5153  elrn  5162  rnopab  5166  brres  5199  brresg  5201  resieq  5203  opelresi  5204  iss  5236  dfres2  5240  restidsing  5244  dfima3  5254  elima3  5258  imai  5263  elimasn  5276  elimasni  5278  eliniseg  5280  cotr  5292  issref  5293  cnvsym  5294  intasym  5295  asymref  5296  asymref2  5297  intirr  5298  codir  5300  qfto  5301  poirr2  5304  xpdifid  5348  sofld  5368  dmsnn0  5386  coiun  5429  co02  5433  coi1  5435  dffun4  5512  dffun5  5513  funeu2  5525  funopab  5533  funcnvsn  5545  isarep1  5579  fnop  5596  fneu2  5598  brprcneu  5766  dffv3  5769  tz6.12  5790  funopfv  5814  fnopfvb  5816  opabiota  5837  dffv2  5847  fvopab5  5878  funfvbrb  5899  dff3  5939  dff4  5940  f1ompt  5948  idref  6041  foeqcnvco  6081  f1eqcocnv  6082  fliftel  6085  fliftel1  6086  fliftcnv  6087  f1oiso  6125  ovprc  6201  brabv  6215  elrnmpt2res  6288  resiexg  6598  1st2ndbr  6707  bropopvvv  6737  frxp  6766  xporderlem  6767  cnvimadfsn  6783  brovex  6824  isprmpt2  6827  ottpos  6839  dftpos3  6847  dftpos4  6848  tposoprab  6865  tfrlem7  6926  tfrlem9a  6929  seqomlem2  6990  seqomlem3  6991  seqomlem4  6992  0we1  7030  brwitnlem  7031  ercnv  7206  brdifun  7212  swoord1  7214  swoord2  7215  0er  7220  elecg  7223  iiner  7256  brecop  7277  brsdom  7416  brdom2  7423  idssen  7438  xpcomco  7485  omxpenlem  7496  brsdom2  7519  infxpenlem  8265  dcomex  8701  brdom3  8780  brdom7disj  8783  brdom6disj  8784  fpwwe2lem8  8889  fpwwe2lem9  8890  fpwwe2lem12  8893  canthwe  8903  dmrecnq  9222  xrlenlt  9527  climcau  13234  caucvgb  13243  divides  13623  vdwpc  14127  isstruct  14270  prdsleval  14501  imasaddfnlem  14552  imasvscafn  14561  invsym2  14787  funcf1  14862  funcixp  14863  funcid  14866  funcco  14867  funcsect  14868  funcinv  14869  funciso  14870  funcoppc  14871  idfucl  14877  cofuval2  14883  cofucl  14884  funcres  14892  funcres2b  14893  funcres2  14894  wunfunc  14895  funcpropd  14896  funcres2c  14897  isfull  14906  isfth  14910  fthsect  14921  fthinv  14922  fthmon  14923  fthepi  14924  ffthiso  14925  fthres2  14928  idffth  14929  cofull  14930  cofth  14931  ressffth  14934  isnat  14943  natixp  14948  nati  14951  elhomai2  14988  homa1  14991  homahom2  14992  eldmcoa  15019  coapm  15025  catcisolem  15060  catciso  15061  1stfcl  15093  2ndfcl  15094  prfcl  15099  evlfcl  15118  curf1cl  15124  curfcl  15128  hofcl  15155  yonedalem1  15168  yonedalem21  15169  yonedalem22  15174  yonffthlem  15178  yoniso  15181  pospo  15229  efgi  16304  efgi2  16310  gsum2d2lem  16554  dmdprd  16569  dprdval  16574  eldprd  16575  dprdvalOLD  16576  eldprdOLD  16577  dprd2dlem2  16628  dprd2dlem1  16629  dprd2da  16630  dprd2d2  16632  isunit  16839  subrgdvds  16969  opsrtoslem2  17657  eltopspOLD  18623  tpsexOLD  18624  lmrcl  18935  lmff  19005  2ndcctbss  19159  2ndcdisj  19160  hausdiag  19318  hauseqlcld  19319  cnextfun  19736  cnextfvval  19737  tgphaus  19787  utop2nei  19925  utop3cls  19926  ucnima  19956  xmeterval  20107  metustidOLD  20234  metustid  20235  metustsymOLD  20236  metustsym  20237  metustexhalfOLD  20238  metustexhalf  20239  elbl4  20251  metuel2  20254  isphtpc  20666  ovolfcl  21050  ovollb2lem  21071  ovolctb  21073  ovolshftlem1  21092  ovolscalem1  21096  ovolicc1  21099  ioombl1lem1  21139  ioorf  21153  dyadf  21171  eldv  21473  dvres2  21487  dvef  21552  eltayl  21925  ulmscl  21944  tglngne  23087  tgelrnln  23142  tghilbert1_1  23149  isperp  23215  brbtwn  23264  iswlk  23545  istrl  23555  ispth  23586  isspth  23587  ex-br  23757  avril1  23775  helloworld  23777  isrngo  23984  rngoablo2  24028  isdivrngo  24037  vcex  24077  h2hlm  24501  axhcompl-zf  24519  opabdm  26061  opabrn  26062  fpwrelmap  26151  isarchi  26317  gsummpt2co  26367  prsdm  26462  prsrn  26463  relexpindlem  27459  dfrtrclrec2  27463  rtrclreclem.trans  27466  brtpid1  27495  brtpid2  27496  brtpid3  27497  brtp  27677  dfso2  27682  dfpo2  27683  fundmpss  27695  opelco3  27707  elpredim  27755  elpredg  27757  wfrlem11  27852  frrlem5c  27892  brsymdif  27977  brv  28026  pprodss4v  28033  brsset  28038  brtxpsd  28043  sscoid  28062  dffun10  28063  brimg  28086  funpartfun  28092  funpartfv  28094  dfrdg4  28099  imagesset  28102  fvtransport  28181  brcolinear2  28207  colineardim1  28210  fvray  28290  fvline  28293  mblfinlem2  28551  areacirclem5  28610  eltail  28717  heiborlem3  28834  heiborlem4  28835  heiborlem6  28837  brabsb2  29129  eqbrrdv2  29130  afveu  30181  fnopafvb  30183  tz6.12-afv  30201  tz6.12-1-afv  30202  aovprc  30216  aovrcl  30217  oprabv  30279  wlkcomp  30408  2wlkeq  30410  wlkcpr  30412  wlknwwlknsur  30466  wlkiswwlksur  30473  isclwlk0  30541  clwlkswlks  30545  clwlkcomp  30548  wlkp1lenfislenp  30634  clwlkfoclwwlk  30640  isrgra  30665  isrusgra  30666  cmtvalN  33137  cvrval  33195
  Copyright terms: Public domain W3C validator