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

Definition df-br 5144
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 11300 for the specific definition of <). As a wff, relations are true or false. For example, (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩} → 3𝑅9) (ex-br 30450). Often class 𝑅 meets the Rel criteria to be defined in df-rel 5692, and in particular 𝑅 may be a function (see df-fun 6563). 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 7933). (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 5143 . 2 wff 𝐴𝑅𝐵
51, 2cop 4632 . . 3 class 𝐴, 𝐵
65, 3wcel 2108 . 2 wff 𝐴, 𝐵⟩ ∈ 𝑅
74, 6wb 206 1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Colors of variables: wff setvar class
This definition is referenced by:  breq  5145  breq1  5146  breq2  5147  ssbrd  5186  nfbrd  5189  br0  5192  brne0  5193  brun  5194  brin  5195  brdif  5196  brsymdif  5202  opabss  5207  brv  5477  brsnop  5527  brtp  5528  brabsb  5536  brabga  5539  elopabrOLD  5568  rbropapd  5569  brabv  5573  epelg  5585  pofun  5610  brxp  5734  opelinxp  5765  bropaex12  5777  brab2a  5779  ssrel3  5796  eqbrriv  5801  eqbrrdv  5803  eqbrrdiv  5804  opeliunxp2  5849  opelco2g  5878  opelco  5882  elcnv2  5888  opelcnvg  5891  dfdm3  5898  dfrn3  5900  elrng  5902  eldm2g  5910  breldm  5919  dmopab  5926  opelrn  5954  rnopab  5965  brres  6004  resieq  6008  opelidres  6009  iss  6053  dfres2  6059  elidinxp  6062  restidsing  6071  dfima3  6081  elima3  6085  imai  6092  elimasng  6107  cotrgOLDOLD  6129  idrefALT  6131  cnvsymOLDOLD  6134  intasym  6135  asymref  6136  asymref2  6137  intirr  6138  codir  6140  qfto  6141  poirr2  6144  xpdifid  6188  sofld  6207  dmsnn0  6227  coiun  6276  coi1  6282  dfpo2  6316  dffun4  6577  dffun5  6578  funeu2  6592  funopab  6601  funcnvsn  6616  isarep1  6656  isarep1OLD  6657  fnop  6677  fneu2  6679  brprcneu  6896  brprcneuALT  6897  dffv3  6902  tz6.12  6931  funopfv  6958  fnopfvb  6960  opabiota  6991  dffv2  7004  fvopab5  7049  funfvbrb  7071  dff3  7120  dff4  7121  f1ompt  7131  idref  7166  foeqcnvco  7320  f1eqcocnv  7321  fliftel  7329  fliftel1  7330  fliftcnv  7331  isof1oopb  7345  f1oiso  7371  ovprc  7469  fnotovb  7483  oprabv  7493  elrnmpores  7571  1st2ndbr  8067  brovpreldm  8114  bropopvvv  8115  frxp  8151  xporderlem  8152  cnvimadfsn  8197  opeliunxp2f  8235  brovex  8247  ottpos  8261  dftpos3  8269  dftpos4  8270  tposoprab  8287  frrlem9  8319  fprresex  8335  wfrfunOLD  8359  wfrlem17OLD  8365  tfrlem7  8423  tfrlem9a  8426  seqomlem2  8491  seqomlem3  8492  seqomlem4  8493  brwitnlem  8545  ercnv  8766  brdifun  8775  swoord1  8777  swoord2  8778  0er  8783  elecg  8789  iiner  8829  brecop  8850  brsdom  9015  brdom2  9022  idssen  9037  xpcomco  9102  omxpenlem  9113  brsdom2  9137  ssttrcl  9755  ttrcltr  9756  ttrclss  9760  infxpenlem  10053  dcomex  10487  brdom7disj  10571  brdom6disj  10572  fpwwe2lem7  10677  fpwwe2lem8  10678  fpwwe2lem11  10681  dmrecnq  11008  xrlenlt  11326  brintclab  15040  brtrclfv  15041  dfrtrclrec2  15097  rtrclreclem3  15099  relexpindlem  15102  climcau  15707  caucvgb  15716  divides  16292  vdwpc  17018  isstruct  17189  setsstruct2  17211  prdsleval  17522  imasaddfnlem  17573  imasvscafn  17582  invsym2  17807  brcic  17842  ciclcl  17846  cicrcl  17847  cicsym  17848  funcf1  17911  funcixp  17912  funcid  17915  funcco  17916  funcsect  17917  funcinv  17918  funciso  17919  funcoppc  17920  idfucl  17926  cofuval2  17932  cofucl  17933  funcres  17941  funcres2b  17942  funcres2  17943  wunfunc  17946  funcpropd  17947  funcres2c  17948  isfull  17957  isfth  17961  fthsect  17972  fthinv  17973  fthmon  17974  fthepi  17975  ffthiso  17976  fthres2  17979  idffth  17980  cofull  17981  cofth  17982  ressffth  17985  inclfusubc  17988  isnat  17995  natixp  18000  nati  18003  elhomai2  18079  homa1  18082  homahom2  18083  eldmcoa  18110  coapm  18116  catcisolem  18155  catciso  18156  1stfcl  18242  2ndfcl  18243  prfcl  18248  evlfcl  18267  curf1cl  18273  curfcl  18277  hofcl  18304  yonedalem1  18317  yonedalem21  18318  yonedalem22  18323  yonffthlem  18327  yoniso  18330  pospo  18390  efgi  19737  efgi2  19743  gsum2d2lem  19991  gsumxp2  19998  dmdprd  20018  dprdval  20023  eldprd  20024  dprd2dlem2  20060  dprd2dlem1  20061  dprd2da  20062  dprd2d2  20064  isunit  20373  subrgdvds  20586  funcrngcsetc  20640  funcrngcsetcALT  20641  funcringcsetc  20674  opsrtoslem2  22080  lmrcl  23239  lmff  23309  2ndcctbss  23463  2ndcdisj  23464  hausdiag  23653  hauseqlcld  23654  cnextfun  24072  cnextfvval  24073  cnextfres  24077  tgphaus  24125  utop2nei  24259  utop3cls  24260  ucnima  24290  xmeterval  24442  metustid  24567  metustsym  24568  metustexhalf  24569  elbl4  24576  metuel2  24578  isphtpc  25026  ovolfcl  25501  ovollb2lem  25523  ovolctb  25525  ovolshftlem1  25544  ovolscalem1  25548  ovolicc1  25551  ioombl1lem1  25593  ioorf  25608  dyadf  25626  eldv  25933  dvres2  25947  dvef  26018  eltayl  26401  ulmscl  26422  scutval  27845  dmscut  27856  scutf  27857  madeval2  27892  scutfo  27942  tglngne  28558  tgelrnln  28638  isperp  28720  brbtwn  28914  iswlk  29628  wlkcpr  29647  wlkcomp  29649  wlkeq  29652  wlklenvclwlk  29673  wlkreslem  29687  clwlkcomp  29799  clwlkcompbp  29802  wlkswwlksf1o  29899  clwlkclwwlkflem  30023  clwlkclwwlkfolem  30026  clwlkclwwlkfo  30028  wlkl0  30386  ex-br  30450  avril1  30482  helloworld  30484  vcex  30597  h2hlm  30999  axhcompl-zf  31017  opeldifid  32612  brab2d  32619  brabgaf  32620  opabdm  32623  opabrn  32624  fpwrelmap  32744  gsummpt2co  33051  isarchi  33189  fldextfld1  33700  fldextfld2  33701  fldextrspunlsplem  33723  qtophaus  33835  prsdm  33913  prsrn  33914  acycgr0v  35153  prclisacycgr  35156  mclsax  35574  brtpid1  35721  brtpid2  35722  brtpid3  35723  dfso2  35755  fundmpss  35767  opelco3  35775  pprodss4v  35885  brsset  35890  brtxpsd  35895  sscoid  35914  dffun10  35915  brimg  35938  funpartfun  35944  funpartfv  35946  dfrecs2  35951  dfrdg4  35952  imagesset  35954  fvtransport  36033  brcolinear2  36059  colineardim1  36062  fvray  36142  fvline  36145  eltail  36375  bj-brrelex12ALT  37068  bj-brresdm  37147  brabd0  37148  bj-ideqg  37158  bj-opelidb1ALT  37167  bj-elid7  37172  bj-opelopabid  37188  uncf  37606  uncov  37608  unccur  37610  phpreu  37611  poimirlem26  37653  mblfinlem2  37665  areacirclem5  37719  heiborlem3  37820  heiborlem4  37821  heiborlem6  37823  isrngo  37904  rngoablo2  37916  isdivrngo  37957  brvdif2  38263  brvvdif  38264  elecALTV  38267  inxprnres  38293  brrabga  38342  iss2  38345  brabidgaw  38366  brabidga  38367  brabsb2  38863  eqbrrdv2  38864  cmtvalN  39212  cvrval  39270  tfsconcat0i  43358  undmrnresiss  43617  cnvssco  43619  cotrintab  43627  elimaint  43662  coiun1  43665  elintima  43666  briunov2  43695  brtrclfv2  43740  frege77d  43759  dfhe3  43788  dffrege76  43952  frege97  43973  frege98  43974  frege109  43985  frege110  43986  dffrege115  43991  frege131  44007  frege133  44009  rfovcnvf1od  44017  fsovrfovd  44022  fourierdlem42  46164  ovolval2lem  46658  ovolval4lem2  46665  et-ltneverrefl  46886  natglobalincr  46892  afveu  47165  fnopafvb  47167  tz6.12-afv  47185  tz6.12-1-afv  47186  aovprc  47200  aovrcl  47201  funressndmafv2rn  47235  tz6.12-afv2  47252  tz6.12-1-afv2  47253  dfatopafv2b  47258  fnopafv2b  47261  dfafv23  47265  sprsymrelfolem2  47480  sprsymrelf  47482  prproropf1olem0  47489  prproropf1olem2  47491  isupwlk  48052  rrx2plord  48641  rrx2plordisom  48644  brab2dd  48741  fvconstr  48765  fvconstrn0  48766  fvconstr2  48767  funcrcl2  48912  funcrcl3  48913  upfval3  48935  uprcl2  48941  uprcl3  48942  natrcl2  48950  natrcl3  48951  swapffunca  48990  swapfiso  48991  fuco2el  49007  fuco22natlem  49040  fucoid  49043  fucoid2  49044  fucofunca  49055  precoffunc  49066  thincciso  49102
  Copyright terms: Public domain W3C validator