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

Definition df-br 4453
 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 9654 for the specific definition of ). As a wff, relations are true or false. For example, (ex-br 25152). Often class meets the Rel criteria to be defined in df-rel 5011, and in particular may be a function (see df-fun 5595). 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 6735). (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 4452 . 2
51, 2cop 4035 . . 3
65, 3wcel 1818 . 2
74, 6wb 184 1
 Colors of variables: wff setvar class This definition is referenced by:  breq  4454  breq1  4455  breq2  4456  ssbrd  4493  nfbrd  4495  br0  4498  brne0  4499  brun  4500  brin  4501  brdif  4502  opabss  4513  brabsb  4763  brabga  4766  epelg  4797  pofun  4821  brxp  5035  brab2a  5054  bropaex12  5078  brab2ga  5080  eqbrriv  5103  eqbrrdv  5105  eqbrrdiv  5106  opeliunxp2  5146  opelco2g  5175  opelco  5179  cnvss  5180  elcnv2  5185  opelcnvg  5187  brcnvg  5188  dfdm3  5195  dfrn3  5197  elrng  5199  eldm2g  5204  breldm  5212  dmopab  5218  opelrn  5239  elrn  5248  rnopab  5252  brres  5285  brresg  5287  resieq  5289  opelresi  5290  iss  5326  dfres2  5331  restidsing  5335  dfima3  5345  elima3  5349  imai  5354  elimasn  5367  elimasni  5369  eliniseg  5371  cotrg  5383  issref  5385  cnvsym  5386  intasym  5387  asymref  5388  asymref2  5389  intirr  5390  codir  5392  qfto  5393  poirr2  5396  xpdifid  5440  sofld  5460  dmsnn0  5478  coiun  5522  coi1  5528  dffun4  5605  dffun5  5606  funeu2  5618  funopab  5626  funcnvsn  5638  isarep1  5672  fnop  5689  fneu2  5691  brprcneu  5864  dffv3  5867  tz6.12  5888  funopfv  5912  fnopfvb  5914  opabiota  5936  dffv2  5946  fvopab5  5979  funfvbrb  6000  dff3  6044  dff4  6045  f1ompt  6053  idref  6153  foeqcnvco  6203  f1eqcocnv  6204  fliftel  6207  fliftel1  6208  fliftcnv  6209  f1oiso  6247  ovprc  6326  brabv  6342  oprabv  6345  elrnmpt2res  6416  resiexg  6736  1st2ndbr  6849  bropopvvv  6880  frxp  6910  xporderlem  6911  cnvimadfsn  6927  brovex  6969  isprmpt2  6972  ottpos  6984  dftpos3  6992  dftpos4  6993  tposoprab  7010  tfrlem7  7071  tfrlem9a  7074  seqomlem2  7135  seqomlem3  7136  seqomlem4  7137  brwitnlem  7176  ercnv  7351  brdifun  7357  swoord1  7359  swoord2  7360  0er  7365  elecg  7369  iiner  7402  brecop  7423  brsdom  7558  brdom2  7565  idssen  7580  xpcomco  7627  omxpenlem  7638  brsdom2  7661  infxpenlem  8412  dcomex  8848  brdom7disj  8930  brdom6disj  8931  fpwwe2lem8  9036  fpwwe2lem9  9037  fpwwe2lem12  9040  dmrecnq  9367  xrlenlt  9673  climcau  13493  caucvgb  13502  divides  13988  vdwpc  14498  isstruct  14642  prdsleval  14874  imasaddfnlem  14925  imasvscafn  14934  invsym2  15157  funcf1  15235  funcixp  15236  funcid  15239  funcco  15240  funcsect  15241  funcinv  15242  funciso  15243  funcoppc  15244  idfucl  15250  cofuval2  15256  cofucl  15257  funcres  15265  funcres2b  15266  funcres2  15267  wunfunc  15268  funcpropd  15269  funcres2c  15270  isfull  15279  isfth  15283  fthsect  15294  fthinv  15295  fthmon  15296  fthepi  15297  ffthiso  15298  fthres2  15301  idffth  15302  cofull  15303  cofth  15304  ressffth  15307  isnat  15316  natixp  15321  nati  15324  elhomai2  15361  homa1  15364  homahom2  15365  eldmcoa  15392  coapm  15398  catcisolem  15433  catciso  15434  1stfcl  15466  2ndfcl  15467  prfcl  15472  evlfcl  15491  curf1cl  15497  curfcl  15501  hofcl  15528  yonedalem1  15541  yonedalem21  15542  yonedalem22  15547  yonffthlem  15551  yoniso  15554  pospo  15603  efgi  16737  efgi2  16743  gsum2d2lem  17001  dmdprd  17029  dprdval  17034  eldprd  17035  dprdvalOLD  17036  eldprdOLD  17037  dprd2dlem2  17089  dprd2dlem1  17090  dprd2da  17091  dprd2d2  17093  isunit  17306  subrgdvds  17443  opsrtoslem2  18149  eltopspOLD  19419  tpsexOLD  19420  lmrcl  19732  lmff  19802  2ndcctbss  19956  2ndcdisj  19957  hausdiag  20146  hauseqlcld  20147  cnextfun  20564  cnextfvval  20565  tgphaus  20615  utop2nei  20753  utop3cls  20754  ucnima  20784  xmeterval  20935  metustidOLD  21062  metustid  21063  metustsymOLD  21064  metustsym  21065  metustexhalfOLD  21066  metustexhalf  21067  elbl4  21079  metuel2  21082  isphtpc  21494  ovolfcl  21878  ovollb2lem  21899  ovolctb  21901  ovolshftlem1  21920  ovolscalem1  21924  ovolicc1  21927  ioombl1lem1  21968  ioorf  21982  dyadf  22000  eldv  22302  dvres2  22316  dvef  22381  eltayl  22755  ulmscl  22774  tglngne  23937  tgelrnln  24010  isperp  24089  brbtwn  24202  uhgraop  24304  usgrac  24351  elusuhgra  24368  usgraexmplc  24404  iswlk  24520  wlkcomp  24525  wlkcpr  24529  istrl  24539  ispth  24570  isspth  24571  2wlkeq  24707  wlknwwlknsur  24712  wlkiswwlksur  24719  isclwlk0  24754  clwlkswlks  24758  clwlkcomp  24763  wlklenvclwlk  24839  clwlkfoclwwlk  24845  isrgra  24926  isrusgra  24927  isrusgusrgcl  24933  0eusgraiff0rgracl  24941  ex-br  25152  avril1  25171  helloworld  25173  isrngo  25380  rngoablo2  25424  isdivrngo  25433  vcex  25473  h2hlm  25897  axhcompl-zf  25915  opeldifid  27456  opabdm  27464  opabrn  27465  fpwrelmap  27556  isarchi  27726  gsummpt2co  27771  qtophaus  27839  prsdm  27896  prsrn  27897  mclsax  28929  relexpindlem  29062  dfrtrclrec2  29066  rtrclreclem.trans  29069  brtpid1  29098  brtpid2  29099  brtpid3  29100  brtp  29178  dfso2  29183  dfpo2  29184  fundmpss  29196  opelco3  29208  elpredim  29256  elpredg  29258  wfrlem11  29353  frrlem5c  29393  brsymdif  29478  brv  29527  pprodss4v  29534  brsset  29539  brtxpsd  29544  sscoid  29563  dffun10  29564  brimg  29587  funpartfun  29593  funpartfv  29595  dfrdg4  29600  imagesset  29603  fvtransport  29682  brcolinear2  29708  colineardim1  29711  fvray  29791  fvline  29794  mblfinlem2  30052  areacirclem5  30111  eltail  30192  heiborlem3  30309  heiborlem4  30310  heiborlem6  30312  brabsb2  30603  eqbrrdv2  30604  fourierdlem42  31931  afveu  32238  fnopafvb  32240  tz6.12-afv  32258  tz6.12-1-afv  32259  aovprc  32273  aovrcl  32274  uhgrasiz  32394  isfusgracl  32426  isfusgraclALT  32428  fusgraimpclALT2  32431  usgrafisbaseALT  32440  usgrafisbaseALT2  32441  usgfis  32446  usgfisALT  32450  brcic  32582  ciclcl  32586  cicrcl  32587  cicsym  32588  inclfusubc  32593  funcrngcsetc  32806  funcrngcsetcALT  32807  funcringcsetc  32843  cmtvalN  34936  cvrval  34994  brintclab  37763  elimaint  37764  elintima  37765  dfhe3  37799
 Copyright terms: Public domain W3C validator