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

Definition df-br 5053
 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 1 and 2 (see df-ltxr 10678 for the specific definition of <). As a wff, relations are true or false. For example, (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩} → 3𝑅9) (ex-br 28219). Often class 𝑅 meets the Rel criteria to be defined in df-rel 5549, and in particular 𝑅 may be a function (see df-fun 6345). 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 7613). (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
df-br (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

Detailed syntax breakdown of Definition df-br
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cR . . 3 class 𝑅
41, 2, 3wbr 5052 . 2 wff 𝐴𝑅𝐵
51, 2cop 4556 . . 3 class 𝐴, 𝐵
65, 3wcel 2115 . 2 wff 𝐴, 𝐵⟩ ∈ 𝑅
74, 6wb 209 1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
 Colors of variables: wff setvar class This definition is referenced by:  breq  5054  breq1  5055  breq2  5056  ssbrd  5095  nfbrd  5098  br0  5101  brne0  5102  brun  5103  brin  5104  brdif  5105  brsymdif  5111  opabss  5116  brv  5351  brabsb  5405  brabga  5408  elopabr  5434  rbropapd  5436  brabv  5440  epelg  5453  epelgOLD  5454  pofun  5478  brxp  5588  opelinxp  5618  bropaex12  5629  brab2a  5631  eqbrriv  5651  eqbrrdv  5653  eqbrrdiv  5654  opeliunxp2  5696  opelco2g  5725  opelco  5729  elcnv2  5735  opelcnvg  5738  dfdm3  5745  dfrn3  5747  elrng  5749  eldm2g  5755  breldm  5764  dmopab  5771  opelrn  5800  elrn  5809  rnopab  5813  brres  5847  resieq  5851  opelidres  5852  iss  5890  dfres2  5896  elidinxp  5898  restidsing  5909  dfima3  5919  elima3  5923  imai  5929  elimasn  5941  elimasni  5943  eliniseg  5945  cotrg  5958  idrefALT  5960  cnvsym  5961  intasym  5962  asymref  5963  asymref2  5964  intirr  5965  codir  5967  qfto  5968  poirr2  5971  xpdifid  6012  sofld  6031  dmsnn0  6051  coiun  6096  coi1  6102  elpredim  6147  elpredg  6149  dffun4  6355  dffun5  6356  funeu2  6369  funopab  6378  funcnvsn  6392  isarep1  6430  fnop  6449  fneu2  6451  brprcneu  6653  dffv3  6657  tz6.12  6684  funopfv  6708  fnopfvb  6710  opabiota  6737  dffv2  6747  fvopab5  6791  funfvbrb  6812  dff3  6857  dff4  6858  f1ompt  6866  idref  6899  foeqcnvco  7048  f1eqcocnv  7049  f1eqcocnvOLD  7050  fliftel  7055  fliftel1  7056  fliftcnv  7057  isof1oopb  7071  f1oiso  7097  ovprc  7187  fnotovb  7199  oprabv  7207  elrnmpores  7281  1st2ndbr  7736  brovpreldm  7780  bropopvvv  7781  frxp  7816  xporderlem  7817  cnvimadfsn  7835  opeliunxp2f  7872  brovex  7884  ottpos  7898  dftpos3  7906  dftpos4  7907  tposoprab  7924  wfrfun  7961  wfrlem17  7967  tfrlem7  8015  tfrlem9a  8018  seqomlem2  8083  seqomlem3  8084  seqomlem4  8085  brwitnlem  8128  ercnv  8306  brdifun  8314  swoord1  8316  swoord2  8317  0er  8322  elecg  8328  iiner  8365  brecop  8386  brsdom  8528  brdom2  8535  idssen  8550  xpcomco  8603  omxpenlem  8614  brsdom2  8638  infxpenlem  9437  dcomex  9867  brdom7disj  9951  brdom6disj  9952  fpwwe2lem8  10057  fpwwe2lem9  10058  fpwwe2lem12  10061  dmrecnq  10388  xrlenlt  10704  brintclab  14361  brtrclfv  14362  dfrtrclrec2  14416  rtrclreclem3  14419  relexpindlem  14422  climcau  15027  caucvgb  15036  divides  15609  vdwpc  16314  isstruct  16496  setsstruct2  16521  prdsleval  16750  imasaddfnlem  16801  imasvscafn  16810  invsym2  17033  brcic  17068  ciclcl  17072  cicrcl  17073  cicsym  17074  funcf1  17136  funcixp  17137  funcid  17140  funcco  17141  funcsect  17142  funcinv  17143  funciso  17144  funcoppc  17145  idfucl  17151  cofuval2  17157  cofucl  17158  funcres  17166  funcres2b  17167  funcres2  17168  wunfunc  17169  funcpropd  17170  funcres2c  17171  isfull  17180  isfth  17184  fthsect  17195  fthinv  17196  fthmon  17197  fthepi  17198  ffthiso  17199  fthres2  17202  idffth  17203  cofull  17204  cofth  17205  ressffth  17208  isnat  17217  natixp  17222  nati  17225  elhomai2  17294  homa1  17297  homahom2  17298  eldmcoa  17325  coapm  17331  catcisolem  17366  catciso  17367  1stfcl  17447  2ndfcl  17448  prfcl  17453  evlfcl  17472  curf1cl  17478  curfcl  17482  hofcl  17509  yonedalem1  17522  yonedalem21  17523  yonedalem22  17528  yonffthlem  17532  yoniso  17535  pospo  17583  efgi  18845  efgi2  18851  gsum2d2lem  19093  gsumxp2  19100  dmdprd  19120  dprdval  19125  eldprd  19126  dprd2dlem2  19162  dprd2dlem1  19163  dprd2da  19164  dprd2d2  19166  isunit  19410  subrgdvds  19549  opsrtoslem2  20265  lmrcl  21839  lmff  21909  2ndcctbss  22063  2ndcdisj  22064  hausdiag  22253  hauseqlcld  22254  cnextfun  22672  cnextfvval  22673  cnextfres  22677  tgphaus  22725  utop2nei  22859  utop3cls  22860  ucnima  22890  xmeterval  23042  metustid  23164  metustsym  23165  metustexhalf  23166  elbl4  23173  metuel2  23175  isphtpc  23602  ovolfcl  24073  ovollb2lem  24095  ovolctb  24097  ovolshftlem1  24116  ovolscalem1  24120  ovolicc1  24123  ioombl1lem1  24165  ioorf  24180  dyadf  24198  eldv  24504  dvres2  24518  dvef  24586  eltayl  24958  ulmscl  24977  tglngne  26347  tgelrnln  26427  isperp  26509  brbtwn  26696  iswlk  27403  wlkcpr  27421  wlkcomp  27423  wlkeq  27426  wlklenvclwlk  27447  wlklenvclwlkOLD  27448  wlkreslem  27462  clwlkcomp  27571  clwlkcompbp  27574  wlkswwlksf1o  27668  clwlkclwwlkflem  27792  clwlkclwwlkfolem  27795  clwlkclwwlkfo  27797  wlkl0  28155  ex-br  28219  avril1  28251  helloworld  28253  vcex  28364  h2hlm  28766  axhcompl-zf  28784  opeldifid  30360  brabgaf  30370  opabdm  30373  opabrn  30374  brsnop  30440  fpwrelmap  30480  gsummpt2co  30718  isarchi  30843  fldextfld1  31099  fldextfld2  31100  qtophaus  31160  prsdm  31214  prsrn  31215  acycgr0v  32452  prclisacycgr  32455  mclsax  32873  brtpid1  33008  brtpid2  33009  brtpid3  33010  brtp  33042  dfso2  33047  dfpo2  33048  fundmpss  33066  opelco3  33075  frrlem9  33188  scutval  33322  dmscut  33329  scutf  33330  madeval2  33347  pprodss4v  33402  brsset  33407  brtxpsd  33412  sscoid  33431  dffun10  33432  brimg  33455  funpartfun  33461  funpartfv  33463  dfrecs2  33468  dfrdg4  33469  imagesset  33471  fvtransport  33550  brcolinear2  33576  colineardim1  33579  fvray  33659  fvline  33662  eltail  33779  bj-brrelex12ALT  34427  bj-brresdm  34506  brabd0  34507  bj-ideqg  34517  bj-opelidb1ALT  34526  bj-elid7  34531  bj-opelopabid  34547  uncf  34981  uncov  34983  unccur  34985  phpreu  34986  poimirlem26  35028  mblfinlem2  35040  areacirclem5  35094  heiborlem3  35196  heiborlem4  35197  heiborlem6  35199  isrngo  35280  rngoablo2  35292  isdivrngo  35333  brvdif2  35628  brvvdif  35629  elecALTV  35632  inxprnres  35654  ssrel3  35661  brrabga  35703  iss2  35706  brabidgaw  35722  brabidga  35723  brabsb2  36103  eqbrrdv2  36104  cmtvalN  36452  cvrval  36510  undmrnresiss  40220  cnvssco  40222  cotrintab  40230  elimaint  40265  coiun1  40269  elintima  40270  briunov2  40299  brtrclfv2  40344  frege77d  40363  dfhe3  40393  dffrege76  40557  frege97  40578  frege98  40579  frege109  40590  frege110  40591  dffrege115  40596  frege131  40612  frege133  40614  rfovcnvf1od  40622  fsovrfovd  40627  fourierdlem42  42717  ovolval2lem  43208  ovolval4lem2  43215  afveu  43635  fnopafvb  43637  tz6.12-afv  43655  tz6.12-1-afv  43656  aovprc  43670  aovrcl  43671  funressndmafv2rn  43705  tz6.12-afv2  43722  tz6.12-1-afv2  43723  dfatopafv2b  43728  fnopafv2b  43731  dfafv23  43735  sprsymrelfolem2  43936  sprsymrelf  43938  prproropf1olem0  43945  prproropf1olem2  43947  isupwlk  44290  inclfusubc  44417  funcrngcsetc  44548  funcrngcsetcALT  44549  funcringcsetc  44585  rrx2plord  45060  rrx2plordisom  45063
 Copyright terms: Public domain W3C validator