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

Definition df-br 4319
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 9302 for the specific definition of ). As a wff, relations are true or false. For example, (ex-br 22760). Often class meets the Rel criteria to be defined in df-rel 4869, and in particular may be a function (see df-fun 5440). 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 6523). (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 4318 . 2
51, 2cop 3912 . . 3
65, 3wcel 1732 . 2
74, 6wb 178 1
Colors of variables: wff set class
This definition is referenced by:  breq  4320  breq1  4321  breq2  4322  ssbrd  4359  nfbrd  4361  br0  4364  brne0  4365  brun  4366  brin  4367  brdif  4368  sbcbr123  4369  opabss  4379  brabsbOLD  4621  brabsb  4623  brabga  4626  epelg  4654  pofun  4678  brxp  4892  brab2a  4910  brab2ga  4934  eqbrriv  4957  eqbrrdv  4959  eqbrrdiv  4960  opeliunxp2  5000  opelco2g  5029  opelco  5033  cnvss  5034  elcnv2  5039  opelcnvg  5041  brcnvg  5042  dfdm3  5049  dfrn3  5051  elrng  5053  eldm2g  5058  breldm  5066  dmopab  5072  opelrn  5093  elrn  5102  rnopab  5106  brres  5139  brresg  5141  resieq  5143  opelresiOLD  5144  opelresi  5145  iss  5177  dfres2  5181  restidsing  5185  dfima3  5195  elima3  5199  imai  5204  elimasn  5217  elimasni  5219  eliniseg  5221  cotr  5233  issref  5234  cnvsym  5235  intasym  5236  asymref  5237  asymref2  5238  intirr  5239  codir  5241  qfto  5242  poirr2  5245  sofld  5306  dmsnn0  5324  coiun  5367  co02  5371  coi1  5373  dffun4  5450  dffun5  5451  funeu2  5463  funopab  5471  funcnvsn  5481  isarep1  5515  fnop  5532  fneu2  5534  brprcneu  5701  dffv3  5704  tz6.12  5724  funopfv  5747  fnopfvb  5749  opabiota  5770  dffv2  5780  fvopab5  5811  funfvbrb  5832  dff3  5872  dff4  5873  f1ompt  5881  idref  5972  foeqcnvco  6008  f1eqcocnv  6009  fliftel  6012  fliftel1  6013  fliftcnv  6014  f1oiso  6052  ovprc  6130  brabv  6144  resiexg  6524  1st2ndbr  6629  bropopvvv  6659  frxp  6688  xporderlem  6689  brovex  6706  isprmpt2  6709  ottpos  6721  dftpos3  6729  dftpos4  6730  tposoprab  6747  tfrlem9a  6809  seqomlem2  6870  seqomlem3  6871  seqomlem4  6872  0we1  6912  brwitnlem  6913  ercnv  7088  brdifun  7094  swoord1  7096  swoord2  7097  0er  7102  elecg  7105  iiner  7138  brecop  7159  brsdom  7294  brdom2  7301  idssen  7316  xpcomco  7363  omxpenlem  7374  brsdom2  7396  infxpenlem  8066  dcomex  8498  brdom3  8577  brdom7disj  8580  brdom6disj  8581  fpwwe2lem8  8683  fpwwe2lem9  8684  fpwwe2lem12  8687  canthwe  8697  dmrecnq  9016  xrlenlt  9321  climcau  12995  caucvgb  13004  divides  13384  vdwpc  13888  isstruct  14031  prdsleval  14253  imasaddfnlem  14307  imasvscafn  14316  invsym2  14542  funcf1  14617  funcixp  14618  funcid  14621  funcco  14622  funcsect  14623  funcinv  14624  funciso  14625  funcoppc  14626  idfucl  14632  cofuval2  14638  cofucl  14639  funcres  14647  funcres2b  14648  funcres2  14649  wunfunc  14650  funcpropd  14651  funcres2c  14652  isfull  14661  isfth  14665  fthsect  14676  fthinv  14677  fthmon  14678  fthepi  14679  ffthiso  14680  fthres2  14683  idffth  14684  cofull  14685  cofth  14686  ressffth  14689  isnat  14698  natixp  14703  nati  14706  elhomai2  14743  homa1  14746  homahom2  14747  eldmcoa  14774  coapm  14780  catcisolem  14815  catciso  14816  1stfcl  14848  2ndfcl  14849  prfcl  14854  evlfcl  14873  curf1cl  14879  curfcl  14883  hofcl  14910  yonedalem1  14923  yonedalem21  14924  yonedalem22  14929  yonffthlem  14933  yoniso  14936  pospo  14984  efgi  15960  efgi2  15966  gsum2d2lem  16162  dmdprd  16174  dprdval  16176  eldprd  16177  dprd2dlem2  16213  dprd2dlem1  16214  dprd2da  16215  dprd2d2  16217  isunit  16378  subrgdvds  16498  opsrtoslem2  17170  eltopspOLD  17997  tpsexOLD  17998  lmrcl  18309  lmff  18379  2ndcctbss  18533  2ndcdisj  18534  hausdiag  18692  hauseqlcld  18693  cnextfun  19110  cnextfvval  19111  tgphaus  19161  utop2nei  19295  utop3cls  19296  ucnima  19326  xmeterval  19477  metustidOLD  19604  metustid  19605  metustsymOLD  19606  metustsym  19607  metustexhalfOLD  19608  metustexhalf  19609  elbl4  19621  metuel2  19624  isphtpc  20034  ovolfcl  20378  ovollb2lem  20399  ovolctb  20401  ovolshftlem1  20420  ovolscalem1  20424  ovolicc1  20427  ioombl1lem1  20467  ioorf  20480  dyadf  20498  eldv  20800  dvres2  20814  dvef  20879  eltayl  21291  ulmscl  21310  iswlk  22548  istrl  22558  ispth  22589  isspth  22590  ex-br  22760  avril1  22778  helloworld  22780  isrngo  22987  rngoablo2  23031  isdivrngo  23040  vcex  23080  h2hlm  23504  axhcompl-zf  23522  opabdm  25070  opabrn  25071  fpwrelmap  25163  isarchi  25331  gsummpt2co  25409  prsdm  25523  prsrn  25524  relexpindlem  26481  dfrtrclrec2  26485  rtrclreclem.trans  26488  brtpid1  26517  brtpid2  26518  brtpid3  26519  brtp  26711  dfso2  26716  dfpo2  26717  fundmpss  26729  opelco3  26742  elpredim  26790  elpredg  26792  wfrlem11  26887  frrlem5c  26927  brsymdif  27012  brv  27061  pprodss4v  27068  brsset  27073  brtxpsd  27078  sscoid  27097  dffun10  27098  brimg  27121  funpartfun  27127  funpartfv  27129  dfrdg4  27134  imagesset  27137  brbtwn  27177  fvtransport  27305  brcolinear2  27331  colineardim1  27334  fvray  27414  fvline  27417  mblfinlem2  27609  areacirclem5  27668  eltail  27775  heiborlem3  27894  heiborlem4  27895  heiborlem6  27897  brabsb2  28151  eqbrrdv2  28152  afveu  29238  fnopafvb  29240  tz6.12-afv  29258  tz6.12-1-afv  29259  aovprc  29273  aovrcl  29274  oprabv  29338  wlkcomp  29467  2wlkeq  29469  wlkcpr  29471  wlknwwlknsur  29525  wlkiswwlksur  29532  isclwlk0  29600  clwlkswlks  29604  clwlkcomp  29607  wlkp1lenfislenp  29693  clwlkfoclwwlk  29699  isrgra  29724  isrusgra  29725  cmtvalN  31559  cvrval  31617
  Copyright terms: Public domain W3C validator