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 5140
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 11252 for the specific definition of <). As a wff, relations are true or false. For example, (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩} → 3𝑅9) (ex-br 30179). Often class 𝑅 meets the Rel criteria to be defined in df-rel 5674, and in particular 𝑅 may be a function (see df-fun 6536). 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 7898). (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 5139 . 2 wff 𝐴𝑅𝐵
51, 2cop 4627 . . 3 class 𝐴, 𝐵
65, 3wcel 2098 . 2 wff 𝐴, 𝐵⟩ ∈ 𝑅
74, 6wb 205 1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Colors of variables: wff setvar class
This definition is referenced by:  breq  5141  breq1  5142  breq2  5143  ssbrd  5182  nfbrd  5185  br0  5188  brne0  5189  brun  5190  brin  5191  brdif  5192  brsymdif  5198  opabss  5203  brv  5463  brsnop  5513  brtp  5514  brabsb  5522  brabga  5525  elopabrOLD  5554  rbropapd  5555  brabv  5560  epelg  5572  pofun  5597  brxp  5716  opelinxp  5746  bropaex12  5758  brab2a  5760  ssrel3  5777  eqbrriv  5782  eqbrrdv  5784  eqbrrdiv  5785  opeliunxp2  5829  opelco2g  5858  opelco  5862  elcnv2  5868  opelcnvg  5871  dfdm3  5878  dfrn3  5880  elrng  5882  eldm2g  5890  breldm  5899  dmopab  5906  opelrn  5933  rnopab  5944  brres  5979  resieq  5983  opelidres  5984  iss  6026  dfres2  6032  elidinxp  6034  restidsing  6043  dfima3  6053  elima3  6057  imai  6064  elimasng  6078  cotrgOLDOLD  6101  idrefALT  6103  cnvsymOLDOLD  6106  intasym  6107  asymref  6108  asymref2  6109  intirr  6110  codir  6112  qfto  6113  poirr2  6116  xpdifid  6158  sofld  6177  dmsnn0  6197  coiun  6246  coi1  6252  dfpo2  6286  dffun4  6550  dffun5  6551  funeu2  6565  funopab  6574  funcnvsn  6589  isarep1  6628  isarep1OLD  6629  fnop  6649  fneu2  6651  brprcneu  6872  brprcneuALT  6873  dffv3  6878  tz6.12  6907  funopfv  6934  fnopfvb  6936  opabiota  6965  dffv2  6977  fvopab5  7021  funfvbrb  7043  dff3  7092  dff4  7093  f1ompt  7103  idref  7137  foeqcnvco  7291  f1eqcocnv  7292  f1eqcocnvOLD  7293  fliftel  7299  fliftel1  7300  fliftcnv  7301  isof1oopb  7315  f1oiso  7341  ovprc  7440  fnotovb  7452  oprabv  7462  elrnmpores  7539  1st2ndbr  8022  brovpreldm  8070  bropopvvv  8071  frxp  8107  xporderlem  8108  cnvimadfsn  8152  opeliunxp2f  8191  brovex  8203  ottpos  8217  dftpos3  8225  dftpos4  8226  tposoprab  8243  frrlem9  8275  fprresex  8291  wfrfunOLD  8315  wfrlem17OLD  8321  tfrlem7  8379  tfrlem9a  8382  seqomlem2  8447  seqomlem3  8448  seqomlem4  8449  brwitnlem  8503  ercnv  8721  brdifun  8729  swoord1  8731  swoord2  8732  0er  8737  elecg  8743  iiner  8780  brecop  8801  brsdom  8968  brdom2  8975  idssen  8990  xpcomco  9059  omxpenlem  9070  brsdom2  9094  ssttrcl  9707  ttrcltr  9708  ttrclss  9712  infxpenlem  10005  dcomex  10439  brdom7disj  10523  brdom6disj  10524  fpwwe2lem7  10629  fpwwe2lem8  10630  fpwwe2lem11  10633  dmrecnq  10960  xrlenlt  11278  brintclab  14950  brtrclfv  14951  dfrtrclrec2  15007  rtrclreclem3  15009  relexpindlem  15012  climcau  15619  caucvgb  15628  divides  16202  vdwpc  16918  isstruct  17090  setsstruct2  17112  prdsleval  17428  imasaddfnlem  17479  imasvscafn  17488  invsym2  17715  brcic  17750  ciclcl  17754  cicrcl  17755  cicsym  17756  funcf1  17821  funcixp  17822  funcid  17825  funcco  17826  funcsect  17827  funcinv  17828  funciso  17829  funcoppc  17830  idfucl  17836  cofuval2  17842  cofucl  17843  funcres  17851  funcres2b  17852  funcres2  17853  wunfunc  17856  wunfuncOLD  17857  funcpropd  17858  funcres2c  17859  isfull  17868  isfth  17872  fthsect  17883  fthinv  17884  fthmon  17885  fthepi  17886  ffthiso  17887  fthres2  17890  idffth  17891  cofull  17892  cofth  17893  ressffth  17896  inclfusubc  17899  isnat  17906  natixp  17911  nati  17914  elhomai2  17992  homa1  17995  homahom2  17996  eldmcoa  18023  coapm  18029  catcisolem  18068  catciso  18069  1stfcl  18157  2ndfcl  18158  prfcl  18163  evlfcl  18183  curf1cl  18189  curfcl  18193  hofcl  18220  yonedalem1  18233  yonedalem21  18234  yonedalem22  18239  yonffthlem  18243  yoniso  18246  pospo  18306  efgi  19635  efgi2  19641  gsum2d2lem  19889  gsumxp2  19896  dmdprd  19916  dprdval  19921  eldprd  19922  dprd2dlem2  19958  dprd2dlem1  19959  dprd2da  19960  dprd2d2  19962  isunit  20271  subrgdvds  20484  funcrngcsetc  20532  funcrngcsetcALT  20533  funcringcsetc  20566  opsrtoslem2  21948  lmrcl  23079  lmff  23149  2ndcctbss  23303  2ndcdisj  23304  hausdiag  23493  hauseqlcld  23494  cnextfun  23912  cnextfvval  23913  cnextfres  23917  tgphaus  23965  utop2nei  24099  utop3cls  24100  ucnima  24130  xmeterval  24282  metustid  24407  metustsym  24408  metustexhalf  24409  elbl4  24416  metuel2  24418  isphtpc  24864  ovolfcl  25339  ovollb2lem  25361  ovolctb  25363  ovolshftlem1  25382  ovolscalem1  25386  ovolicc1  25389  ioombl1lem1  25431  ioorf  25446  dyadf  25464  eldv  25771  dvres2  25785  dvef  25856  eltayl  26237  ulmscl  26256  scutval  27674  dmscut  27685  scutf  27686  madeval2  27721  scutfo  27771  tglngne  28295  tgelrnln  28375  isperp  28457  brbtwn  28651  iswlk  29362  wlkcpr  29381  wlkcomp  29383  wlkeq  29386  wlklenvclwlk  29407  wlkreslem  29421  clwlkcomp  29531  clwlkcompbp  29534  wlkswwlksf1o  29628  clwlkclwwlkflem  29752  clwlkclwwlkfolem  29755  clwlkclwwlkfo  29757  wlkl0  30115  ex-br  30179  avril1  30211  helloworld  30213  vcex  30326  h2hlm  30728  axhcompl-zf  30746  opeldifid  32325  brabgaf  32332  opabdm  32335  opabrn  32336  fpwrelmap  32453  gsummpt2co  32694  isarchi  32822  fldextfld1  33236  fldextfld2  33237  qtophaus  33336  prsdm  33414  prsrn  33415  acycgr0v  34657  prclisacycgr  34660  mclsax  35078  brtpid1  35214  brtpid2  35215  brtpid3  35216  dfso2  35248  fundmpss  35261  opelco3  35269  pprodss4v  35379  brsset  35384  brtxpsd  35389  sscoid  35408  dffun10  35409  brimg  35432  funpartfun  35438  funpartfv  35440  dfrecs2  35445  dfrdg4  35446  imagesset  35448  fvtransport  35527  brcolinear2  35553  colineardim1  35556  fvray  35636  fvline  35639  eltail  35760  bj-brrelex12ALT  36449  bj-brresdm  36528  brabd0  36529  bj-ideqg  36539  bj-opelidb1ALT  36548  bj-elid7  36553  bj-opelopabid  36569  uncf  36971  uncov  36973  unccur  36975  phpreu  36976  poimirlem26  37018  mblfinlem2  37030  areacirclem5  37084  heiborlem3  37185  heiborlem4  37186  heiborlem6  37188  isrngo  37269  rngoablo2  37281  isdivrngo  37322  brvdif2  37634  brvvdif  37635  elecALTV  37638  inxprnres  37665  brrabga  37714  iss2  37717  brabidgaw  37738  brabidga  37739  brabsb2  38236  eqbrrdv2  38237  cmtvalN  38585  cvrval  38643  tfsconcat0i  42645  undmrnresiss  42905  cnvssco  42907  cotrintab  42915  elimaint  42950  coiun1  42953  elintima  42954  briunov2  42983  brtrclfv2  43028  frege77d  43047  dfhe3  43076  dffrege76  43240  frege97  43261  frege98  43262  frege109  43273  frege110  43274  dffrege115  43279  frege131  43295  frege133  43297  rfovcnvf1od  43305  fsovrfovd  43310  fourierdlem42  45411  ovolval2lem  45905  ovolval4lem2  45912  et-ltneverrefl  46133  natglobalincr  46137  afveu  46407  fnopafvb  46409  tz6.12-afv  46427  tz6.12-1-afv  46428  aovprc  46442  aovrcl  46443  funressndmafv2rn  46477  tz6.12-afv2  46494  tz6.12-1-afv2  46495  dfatopafv2b  46500  fnopafv2b  46503  dfafv23  46507  sprsymrelfolem2  46707  sprsymrelf  46709  prproropf1olem0  46716  prproropf1olem2  46718  isupwlk  47060  rrx2plord  47655  rrx2plordisom  47658  fvconstr  47770  fvconstrn0  47771  fvconstr2  47772  thincciso  47917
  Copyright terms: Public domain W3C validator