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 5148
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 11297 for the specific definition of <). As a wff, relations are true or false. For example, (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩} → 3𝑅9) (ex-br 30459). Often class 𝑅 meets the Rel criteria to be defined in df-rel 5695, and in particular 𝑅 may be a function (see df-fun 6564). 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 5147 . 2 wff 𝐴𝑅𝐵
51, 2cop 4636 . . 3 class 𝐴, 𝐵
65, 3wcel 2105 . 2 wff 𝐴, 𝐵⟩ ∈ 𝑅
74, 6wb 206 1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Colors of variables: wff setvar class
This definition is referenced by:  breq  5149  breq1  5150  breq2  5151  ssbrd  5190  nfbrd  5193  br0  5196  brne0  5197  brun  5198  brin  5199  brdif  5200  brsymdif  5206  opabss  5211  brv  5482  brsnop  5531  brtp  5532  brabsb  5540  brabga  5543  elopabrOLD  5572  rbropapd  5573  brabv  5577  epelg  5589  pofun  5614  brxp  5737  opelinxp  5767  bropaex12  5779  brab2a  5781  ssrel3  5798  eqbrriv  5803  eqbrrdv  5805  eqbrrdiv  5806  opeliunxp2  5851  opelco2g  5880  opelco  5884  elcnv2  5890  opelcnvg  5893  dfdm3  5900  dfrn3  5902  elrng  5904  eldm2g  5912  breldm  5921  dmopab  5928  opelrn  5956  rnopab  5967  brres  6006  resieq  6010  opelidres  6011  iss  6054  dfres2  6060  elidinxp  6063  restidsing  6072  dfima3  6082  elima3  6086  imai  6093  elimasng  6108  cotrgOLDOLD  6131  idrefALT  6133  cnvsymOLDOLD  6136  intasym  6137  asymref  6138  asymref2  6139  intirr  6140  codir  6142  qfto  6143  poirr2  6146  xpdifid  6189  sofld  6208  dmsnn0  6228  coiun  6277  coi1  6283  dfpo2  6317  dffun4  6578  dffun5  6579  funeu2  6593  funopab  6602  funcnvsn  6617  isarep1  6656  isarep1OLD  6657  fnop  6677  fneu2  6679  brprcneu  6896  brprcneuALT  6897  dffv3  6902  tz6.12  6931  funopfv  6958  fnopfvb  6960  opabiota  6990  dffv2  7003  fvopab5  7048  funfvbrb  7070  dff3  7119  dff4  7120  f1ompt  7130  idref  7165  foeqcnvco  7319  f1eqcocnv  7320  fliftel  7328  fliftel1  7329  fliftcnv  7330  isof1oopb  7344  f1oiso  7370  ovprc  7468  fnotovb  7482  oprabv  7492  elrnmpores  7570  1st2ndbr  8065  brovpreldm  8112  bropopvvv  8113  frxp  8149  xporderlem  8150  cnvimadfsn  8195  opeliunxp2f  8233  brovex  8245  ottpos  8259  dftpos3  8267  dftpos4  8268  tposoprab  8285  frrlem9  8317  fprresex  8333  wfrfunOLD  8357  wfrlem17OLD  8363  tfrlem7  8421  tfrlem9a  8424  seqomlem2  8489  seqomlem3  8490  seqomlem4  8491  brwitnlem  8543  ercnv  8764  brdifun  8773  swoord1  8775  swoord2  8776  0er  8781  elecg  8787  iiner  8827  brecop  8848  brsdom  9013  brdom2  9020  idssen  9035  xpcomco  9100  omxpenlem  9111  brsdom2  9135  ssttrcl  9752  ttrcltr  9753  ttrclss  9757  infxpenlem  10050  dcomex  10484  brdom7disj  10568  brdom6disj  10569  fpwwe2lem7  10674  fpwwe2lem8  10675  fpwwe2lem11  10678  dmrecnq  11005  xrlenlt  11323  brintclab  15036  brtrclfv  15037  dfrtrclrec2  15093  rtrclreclem3  15095  relexpindlem  15098  climcau  15703  caucvgb  15712  divides  16288  vdwpc  17013  isstruct  17185  setsstruct2  17207  prdsleval  17523  imasaddfnlem  17574  imasvscafn  17583  invsym2  17810  brcic  17845  ciclcl  17849  cicrcl  17850  cicsym  17851  funcf1  17916  funcixp  17917  funcid  17920  funcco  17921  funcsect  17922  funcinv  17923  funciso  17924  funcoppc  17925  idfucl  17931  cofuval2  17937  cofucl  17938  funcres  17946  funcres2b  17947  funcres2  17948  wunfunc  17951  wunfuncOLD  17952  funcpropd  17953  funcres2c  17954  isfull  17963  isfth  17967  fthsect  17978  fthinv  17979  fthmon  17980  fthepi  17981  ffthiso  17982  fthres2  17985  idffth  17986  cofull  17987  cofth  17988  ressffth  17991  inclfusubc  17994  isnat  18001  natixp  18006  nati  18009  elhomai2  18087  homa1  18090  homahom2  18091  eldmcoa  18118  coapm  18124  catcisolem  18163  catciso  18164  1stfcl  18252  2ndfcl  18253  prfcl  18258  evlfcl  18278  curf1cl  18284  curfcl  18288  hofcl  18315  yonedalem1  18328  yonedalem21  18329  yonedalem22  18334  yonffthlem  18338  yoniso  18341  pospo  18402  efgi  19751  efgi2  19757  gsum2d2lem  20005  gsumxp2  20012  dmdprd  20032  dprdval  20037  eldprd  20038  dprd2dlem2  20074  dprd2dlem1  20075  dprd2da  20076  dprd2d2  20078  isunit  20389  subrgdvds  20602  funcrngcsetc  20656  funcrngcsetcALT  20657  funcringcsetc  20690  opsrtoslem2  22097  lmrcl  23254  lmff  23324  2ndcctbss  23478  2ndcdisj  23479  hausdiag  23668  hauseqlcld  23669  cnextfun  24087  cnextfvval  24088  cnextfres  24092  tgphaus  24140  utop2nei  24274  utop3cls  24275  ucnima  24305  xmeterval  24457  metustid  24582  metustsym  24583  metustexhalf  24584  elbl4  24591  metuel2  24593  isphtpc  25039  ovolfcl  25514  ovollb2lem  25536  ovolctb  25538  ovolshftlem1  25557  ovolscalem1  25561  ovolicc1  25564  ioombl1lem1  25606  ioorf  25621  dyadf  25639  eldv  25947  dvres2  25961  dvef  26032  eltayl  26415  ulmscl  26436  scutval  27859  dmscut  27870  scutf  27871  madeval2  27906  scutfo  27956  tglngne  28572  tgelrnln  28652  isperp  28734  brbtwn  28928  iswlk  29642  wlkcpr  29661  wlkcomp  29663  wlkeq  29666  wlklenvclwlk  29687  wlkreslem  29701  clwlkcomp  29811  clwlkcompbp  29814  wlkswwlksf1o  29908  clwlkclwwlkflem  30032  clwlkclwwlkfolem  30035  clwlkclwwlkfo  30037  wlkl0  30395  ex-br  30459  avril1  30491  helloworld  30493  vcex  30606  h2hlm  31008  axhcompl-zf  31026  opeldifid  32618  brab2d  32626  brabgaf  32627  opabdm  32630  opabrn  32631  fpwrelmap  32750  gsummpt2co  33033  isarchi  33171  fldextfld1  33676  fldextfld2  33677  qtophaus  33796  prsdm  33874  prsrn  33875  acycgr0v  35132  prclisacycgr  35135  mclsax  35553  brtpid1  35700  brtpid2  35701  brtpid3  35702  dfso2  35734  fundmpss  35747  opelco3  35755  pprodss4v  35865  brsset  35870  brtxpsd  35875  sscoid  35894  dffun10  35895  brimg  35918  funpartfun  35924  funpartfv  35926  dfrecs2  35931  dfrdg4  35932  imagesset  35934  fvtransport  36013  brcolinear2  36039  colineardim1  36042  fvray  36122  fvline  36125  eltail  36356  bj-brrelex12ALT  37049  bj-brresdm  37128  brabd0  37129  bj-ideqg  37139  bj-opelidb1ALT  37148  bj-elid7  37153  bj-opelopabid  37169  uncf  37585  uncov  37587  unccur  37589  phpreu  37590  poimirlem26  37632  mblfinlem2  37644  areacirclem5  37698  heiborlem3  37799  heiborlem4  37800  heiborlem6  37802  isrngo  37883  rngoablo2  37895  isdivrngo  37936  brvdif2  38243  brvvdif  38244  elecALTV  38247  inxprnres  38273  brrabga  38322  iss2  38325  brabidgaw  38346  brabidga  38347  brabsb2  38843  eqbrrdv2  38844  cmtvalN  39192  cvrval  39250  tfsconcat0i  43334  undmrnresiss  43593  cnvssco  43595  cotrintab  43603  elimaint  43638  coiun1  43641  elintima  43642  briunov2  43671  brtrclfv2  43716  frege77d  43735  dfhe3  43764  dffrege76  43928  frege97  43949  frege98  43950  frege109  43961  frege110  43962  dffrege115  43967  frege131  43983  frege133  43985  rfovcnvf1od  43993  fsovrfovd  43998  fourierdlem42  46104  ovolval2lem  46598  ovolval4lem2  46605  et-ltneverrefl  46826  natglobalincr  46830  afveu  47102  fnopafvb  47104  tz6.12-afv  47122  tz6.12-1-afv  47123  aovprc  47137  aovrcl  47138  funressndmafv2rn  47172  tz6.12-afv2  47189  tz6.12-1-afv2  47190  dfatopafv2b  47195  fnopafv2b  47198  dfafv23  47202  sprsymrelfolem2  47417  sprsymrelf  47419  prproropf1olem0  47426  prproropf1olem2  47428  isupwlk  47979  rrx2plord  48569  rrx2plordisom  48572  fvconstr  48685  fvconstrn0  48686  fvconstr2  48687  funcrcl2  48808  funcrcl3  48809  thincciso  48848
  Copyright terms: Public domain W3C validator