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 5149
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 11284 for the specific definition of <). As a wff, relations are true or false. For example, (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩} → 3𝑅9) (ex-br 30254). Often class 𝑅 meets the Rel criteria to be defined in df-rel 5685, and in particular 𝑅 may be a function (see df-fun 6550). 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 7919). (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 5148 . 2 wff 𝐴𝑅𝐵
51, 2cop 4635 . . 3 class 𝐴, 𝐵
65, 3wcel 2099 . 2 wff 𝐴, 𝐵⟩ ∈ 𝑅
74, 6wb 205 1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Colors of variables: wff setvar class
This definition is referenced by:  breq  5150  breq1  5151  breq2  5152  ssbrd  5191  nfbrd  5194  br0  5197  brne0  5198  brun  5199  brin  5200  brdif  5201  brsymdif  5207  opabss  5212  brv  5474  brsnop  5524  brtp  5525  brabsb  5533  brabga  5536  elopabrOLD  5565  rbropapd  5566  brabv  5571  epelg  5583  pofun  5608  brxp  5727  opelinxp  5757  bropaex12  5769  brab2a  5771  ssrel3  5788  eqbrriv  5793  eqbrrdv  5795  eqbrrdiv  5796  opeliunxp2  5841  opelco2g  5870  opelco  5874  elcnv2  5880  opelcnvg  5883  dfdm3  5890  dfrn3  5892  elrng  5894  eldm2g  5902  breldm  5911  dmopab  5918  opelrn  5945  rnopab  5956  brres  5992  resieq  5996  opelidres  5997  iss  6039  dfres2  6045  elidinxp  6047  restidsing  6056  dfima3  6066  elima3  6070  imai  6077  elimasng  6092  cotrgOLDOLD  6115  idrefALT  6117  cnvsymOLDOLD  6120  intasym  6121  asymref  6122  asymref2  6123  intirr  6124  codir  6126  qfto  6127  poirr2  6130  xpdifid  6172  sofld  6191  dmsnn0  6211  coiun  6260  coi1  6266  dfpo2  6300  dffun4  6564  dffun5  6565  funeu2  6579  funopab  6588  funcnvsn  6603  isarep1  6642  isarep1OLD  6643  fnop  6663  fneu2  6665  brprcneu  6887  brprcneuALT  6888  dffv3  6893  tz6.12  6922  funopfv  6949  fnopfvb  6951  opabiota  6981  dffv2  6993  fvopab5  7038  funfvbrb  7060  dff3  7110  dff4  7111  f1ompt  7121  idref  7155  foeqcnvco  7309  f1eqcocnv  7310  f1eqcocnvOLD  7311  fliftel  7317  fliftel1  7318  fliftcnv  7319  isof1oopb  7333  f1oiso  7359  ovprc  7458  fnotovb  7470  oprabv  7480  elrnmpores  7559  1st2ndbr  8046  brovpreldm  8094  bropopvvv  8095  frxp  8131  xporderlem  8132  cnvimadfsn  8177  opeliunxp2f  8216  brovex  8228  ottpos  8242  dftpos3  8250  dftpos4  8251  tposoprab  8268  frrlem9  8300  fprresex  8316  wfrfunOLD  8340  wfrlem17OLD  8346  tfrlem7  8404  tfrlem9a  8407  seqomlem2  8472  seqomlem3  8473  seqomlem4  8474  brwitnlem  8528  ercnv  8746  brdifun  8754  swoord1  8756  swoord2  8757  0er  8762  elecg  8768  iiner  8808  brecop  8829  brsdom  8996  brdom2  9003  idssen  9018  xpcomco  9087  omxpenlem  9098  brsdom2  9122  ssttrcl  9739  ttrcltr  9740  ttrclss  9744  infxpenlem  10037  dcomex  10471  brdom7disj  10555  brdom6disj  10556  fpwwe2lem7  10661  fpwwe2lem8  10662  fpwwe2lem11  10665  dmrecnq  10992  xrlenlt  11310  brintclab  14981  brtrclfv  14982  dfrtrclrec2  15038  rtrclreclem3  15040  relexpindlem  15043  climcau  15650  caucvgb  15659  divides  16233  vdwpc  16949  isstruct  17121  setsstruct2  17143  prdsleval  17459  imasaddfnlem  17510  imasvscafn  17519  invsym2  17746  brcic  17781  ciclcl  17785  cicrcl  17786  cicsym  17787  funcf1  17852  funcixp  17853  funcid  17856  funcco  17857  funcsect  17858  funcinv  17859  funciso  17860  funcoppc  17861  idfucl  17867  cofuval2  17873  cofucl  17874  funcres  17882  funcres2b  17883  funcres2  17884  wunfunc  17887  wunfuncOLD  17888  funcpropd  17889  funcres2c  17890  isfull  17899  isfth  17903  fthsect  17914  fthinv  17915  fthmon  17916  fthepi  17917  ffthiso  17918  fthres2  17921  idffth  17922  cofull  17923  cofth  17924  ressffth  17927  inclfusubc  17930  isnat  17937  natixp  17942  nati  17945  elhomai2  18023  homa1  18026  homahom2  18027  eldmcoa  18054  coapm  18060  catcisolem  18099  catciso  18100  1stfcl  18188  2ndfcl  18189  prfcl  18194  evlfcl  18214  curf1cl  18220  curfcl  18224  hofcl  18251  yonedalem1  18264  yonedalem21  18265  yonedalem22  18270  yonffthlem  18274  yoniso  18277  pospo  18337  efgi  19674  efgi2  19680  gsum2d2lem  19928  gsumxp2  19935  dmdprd  19955  dprdval  19960  eldprd  19961  dprd2dlem2  19997  dprd2dlem1  19998  dprd2da  19999  dprd2d2  20001  isunit  20312  subrgdvds  20525  funcrngcsetc  20573  funcrngcsetcALT  20574  funcringcsetc  20607  opsrtoslem2  22000  lmrcl  23148  lmff  23218  2ndcctbss  23372  2ndcdisj  23373  hausdiag  23562  hauseqlcld  23563  cnextfun  23981  cnextfvval  23982  cnextfres  23986  tgphaus  24034  utop2nei  24168  utop3cls  24169  ucnima  24199  xmeterval  24351  metustid  24476  metustsym  24477  metustexhalf  24478  elbl4  24485  metuel2  24487  isphtpc  24933  ovolfcl  25408  ovollb2lem  25430  ovolctb  25432  ovolshftlem1  25451  ovolscalem1  25455  ovolicc1  25458  ioombl1lem1  25500  ioorf  25515  dyadf  25533  eldv  25840  dvres2  25854  dvef  25925  eltayl  26307  ulmscl  26328  scutval  27746  dmscut  27757  scutf  27758  madeval2  27793  scutfo  27843  tglngne  28367  tgelrnln  28447  isperp  28529  brbtwn  28723  iswlk  29437  wlkcpr  29456  wlkcomp  29458  wlkeq  29461  wlklenvclwlk  29482  wlkreslem  29496  clwlkcomp  29606  clwlkcompbp  29609  wlkswwlksf1o  29703  clwlkclwwlkflem  29827  clwlkclwwlkfolem  29830  clwlkclwwlkfo  29832  wlkl0  30190  ex-br  30254  avril1  30286  helloworld  30288  vcex  30401  h2hlm  30803  axhcompl-zf  30821  opeldifid  32402  brab2d  32410  brabgaf  32411  opabdm  32414  opabrn  32415  fpwrelmap  32528  gsummpt2co  32775  isarchi  32903  fldextfld1  33341  fldextfld2  33342  qtophaus  33437  prsdm  33515  prsrn  33516  acycgr0v  34758  prclisacycgr  34761  mclsax  35179  brtpid1  35315  brtpid2  35316  brtpid3  35317  dfso2  35349  fundmpss  35362  opelco3  35370  pprodss4v  35480  brsset  35485  brtxpsd  35490  sscoid  35509  dffun10  35510  brimg  35533  funpartfun  35539  funpartfv  35541  dfrecs2  35546  dfrdg4  35547  imagesset  35549  fvtransport  35628  brcolinear2  35654  colineardim1  35657  fvray  35737  fvline  35740  eltail  35858  bj-brrelex12ALT  36546  bj-brresdm  36625  brabd0  36626  bj-ideqg  36636  bj-opelidb1ALT  36645  bj-elid7  36650  bj-opelopabid  36666  uncf  37072  uncov  37074  unccur  37076  phpreu  37077  poimirlem26  37119  mblfinlem2  37131  areacirclem5  37185  heiborlem3  37286  heiborlem4  37287  heiborlem6  37289  isrngo  37370  rngoablo2  37382  isdivrngo  37423  brvdif2  37734  brvvdif  37735  elecALTV  37738  inxprnres  37764  brrabga  37813  iss2  37816  brabidgaw  37837  brabidga  37838  brabsb2  38334  eqbrrdv2  38335  cmtvalN  38683  cvrval  38741  tfsconcat0i  42774  undmrnresiss  43034  cnvssco  43036  cotrintab  43044  elimaint  43079  coiun1  43082  elintima  43083  briunov2  43112  brtrclfv2  43157  frege77d  43176  dfhe3  43205  dffrege76  43369  frege97  43390  frege98  43391  frege109  43402  frege110  43403  dffrege115  43408  frege131  43424  frege133  43426  rfovcnvf1od  43434  fsovrfovd  43439  fourierdlem42  45537  ovolval2lem  46031  ovolval4lem2  46038  et-ltneverrefl  46259  natglobalincr  46263  afveu  46533  fnopafvb  46535  tz6.12-afv  46553  tz6.12-1-afv  46554  aovprc  46568  aovrcl  46569  funressndmafv2rn  46603  tz6.12-afv2  46620  tz6.12-1-afv2  46621  dfatopafv2b  46626  fnopafv2b  46629  dfafv23  46633  sprsymrelfolem2  46833  sprsymrelf  46835  prproropf1olem0  46842  prproropf1olem2  46844  isupwlk  47198  rrx2plord  47793  rrx2plordisom  47796  fvconstr  47908  fvconstrn0  47909  fvconstr2  47910  thincciso  48055
  Copyright terms: Public domain W3C validator