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 4578
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 9935 for the specific definition of <). As a wff, relations are true or false. For example, (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩} → 3𝑅9) (ex-br 26473). Often class 𝑅 meets the Rel criteria to be defined in df-rel 5034, and in particular 𝑅 may be a function (see df-fun 5791). 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 6970). (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 4577 . 2 wff 𝐴𝑅𝐵
51, 2cop 4130 . . 3 class 𝐴, 𝐵
65, 3wcel 1976 . 2 wff 𝐴, 𝐵⟩ ∈ 𝑅
74, 6wb 194 1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Colors of variables: wff setvar class
This definition is referenced by:  breq  4579  breq1  4580  breq2  4581  ssbrd  4620  nfbrd  4622  br0  4625  brne0  4626  brun  4627  brin  4628  brdif  4629  brsymdif  4635  opabss  4640  brabsb  4900  brabga  4903  elopabr  4926  rbropapd  4928  epelg  4939  pofun  4964  brxp  5060  brab2a  5080  bropaex12  5104  brab2ga  5106  eqbrriv  5126  eqbrrdv  5128  eqbrrdiv  5129  opeliunxp2  5169  opelco2g  5198  opelco  5202  cnvssOLD  5204  elcnv2  5209  opelcnvg  5211  brcnvg  5212  dfdm3  5219  dfrn3  5221  elrng  5223  eldm2g  5228  breldm  5237  dmopab  5243  opelrn  5264  elrn  5273  rnopab  5277  brres  5309  brresg  5311  resieq  5313  opelresi  5314  iss  5353  dfres2  5358  restidsing  5363  restidsingOLD  5364  dfima3  5374  elima3  5378  imai  5383  elimasn  5395  elimasni  5397  eliniseg  5399  cotrg  5412  issref  5414  cnvsym  5415  intasym  5416  asymref  5417  asymref2  5418  intirr  5419  codir  5421  qfto  5422  poirr2  5425  xpdifid  5466  sofld  5485  dmsnn0  5503  coiun  5547  coi1  5553  elpredim  5594  elpredg  5596  dffun4  5801  dffun5  5802  funeu2  5814  funopab  5822  funcnvsn  5835  isarep1  5876  fnop  5893  fneu2  5895  brprcneu  6080  dffv3  6083  tz6.12  6105  funopfv  6129  fnopfvb  6131  opabiota  6155  dffv2  6165  fvopab5  6201  funfvbrb  6222  dff3  6264  dff4  6265  f1ompt  6274  idref  6380  foeqcnvco  6432  f1eqcocnv  6433  fliftel  6436  fliftel1  6437  fliftcnv  6438  isof1oopb  6452  f1oiso  6478  ovprc  6558  brabv  6574  oprabv  6578  elrnmpt2res  6649  resiexg  6971  1st2ndbr  7085  brovpreldm  7118  bropopvvv  7119  frxp  7151  xporderlem  7152  cnvimadfsn  7168  opeliunxp2f  7200  brovex  7212  ottpos  7226  dftpos3  7234  dftpos4  7235  tposoprab  7252  wfrfun  7289  wfrlem17  7295  tfrlem7  7343  tfrlem9a  7346  seqomlem2  7410  seqomlem3  7411  seqomlem4  7412  brwitnlem  7451  ercnv  7627  brdifun  7635  swoord1  7637  swoord2  7638  0er  7644  0erOLD  7645  elecg  7649  iiner  7683  brecop  7704  brsdom  7841  brdom2  7848  idssen  7863  xpcomco  7912  omxpenlem  7923  brsdom2  7946  infxpenlem  8696  dcomex  9129  brdom7disj  9211  brdom6disj  9212  fpwwe2lem8  9315  fpwwe2lem9  9316  fpwwe2lem12  9319  dmrecnq  9646  xrlenlt  9954  brintclab  13538  brtrclfv  13539  dfrtrclrec2  13593  rtrclreclem3  13596  relexpindlem  13599  climcau  14197  caucvgb  14206  divides  14771  vdwpc  15470  isstruct  15653  prdsleval  15908  imasaddfnlem  15959  imasvscafn  15968  invsym2  16194  brcic  16229  ciclcl  16233  cicrcl  16234  cicsym  16235  funcf1  16297  funcixp  16298  funcid  16301  funcco  16302  funcsect  16303  funcinv  16304  funciso  16305  funcoppc  16306  idfucl  16312  cofuval2  16318  cofucl  16319  funcres  16327  funcres2b  16328  funcres2  16329  wunfunc  16330  funcpropd  16331  funcres2c  16332  isfull  16341  isfth  16345  fthsect  16356  fthinv  16357  fthmon  16358  fthepi  16359  ffthiso  16360  fthres2  16363  idffth  16364  cofull  16365  cofth  16366  ressffth  16369  isnat  16378  natixp  16383  nati  16386  elhomai2  16455  homa1  16458  homahom2  16459  eldmcoa  16486  coapm  16492  catcisolem  16527  catciso  16528  1stfcl  16608  2ndfcl  16609  prfcl  16614  evlfcl  16633  curf1cl  16639  curfcl  16643  hofcl  16670  yonedalem1  16683  yonedalem21  16684  yonedalem22  16689  yonffthlem  16693  yoniso  16696  pospo  16744  efgi  17903  efgi2  17909  gsum2d2lem  18143  dmdprd  18168  dprdval  18173  eldprd  18174  dprd2dlem2  18210  dprd2dlem1  18211  dprd2da  18212  dprd2d2  18214  isunit  18428  subrgdvds  18565  opsrtoslem2  19254  lmrcl  20792  lmff  20862  2ndcctbss  21015  2ndcdisj  21016  hausdiag  21205  hauseqlcld  21206  cnextfun  21625  cnextfvval  21626  cnextfres  21630  tgphaus  21677  utop2nei  21811  utop3cls  21812  ucnima  21842  xmeterval  21994  metustid  22116  metustsym  22117  metustexhalf  22118  elbl4  22125  metuel2  22127  isphtpc  22548  ovolfcl  22986  ovollb2lem  23007  ovolctb  23009  ovolshftlem1  23028  ovolscalem1  23032  ovolicc1  23035  ioombl1lem1  23077  ioorf  23091  dyadf  23109  eldv  23412  dvres2  23426  dvef  23491  eltayl  23862  ulmscl  23881  tglngne  25190  tgelrnln  25270  isperp  25352  brbtwn  25524  uhgraop  25626  usgrac  25673  elusuhgra  25690  usgraexmplc  25726  iswlk  25841  wlkcomp  25846  wlkcpr  25850  istrl  25860  ispth  25891  isspth  25892  2wlkeq  26028  wlknwwlknsur  26033  wlkiswwlksur  26040  isclwlk0  26075  clwlkswlks  26079  clwlkcomp  26084  wlklenvclwlk  26159  clwlkfoclwwlk  26165  isrgra  26246  isrusgra  26247  isrusgusrgcl  26253  0eusgraiff0rgracl  26261  ex-br  26473  avril1  26504  helloworld  26506  vcex  26610  h2hlm  27014  axhcompl-zf  27032  opeldifid  28587  brabgaf  28593  opabdm  28596  opabrn  28597  fpwrelmap  28689  isarchi  28860  gsummpt2co  28904  qtophaus  29024  prsdm  29081  prsrn  29082  mclsax  30513  brtpid1  30650  brtpid2  30651  brtpid3  30652  brtp  30685  dfso2  30690  dfpo2  30691  fundmpss  30703  opelco3  30716  frrlem5c  30823  brv  30947  pprodss4v  30954  brsset  30959  brtxpsd  30964  sscoid  30983  dffun10  30984  brimg  31007  funpartfun  31013  funpartfv  31015  dfrecs2  31020  dfrdg4  31021  imagesset  31023  fvtransport  31102  brcolinear2  31128  colineardim1  31131  fvray  31211  fvline  31214  eltail  31332  uncf  32341  uncov  32343  unccur  32345  phpreu  32346  poimirlem26  32388  mblfinlem2  32400  areacirclem5  32457  heiborlem3  32565  heiborlem4  32566  heiborlem6  32568  isrngo  32649  rngoablo2  32661  isdivrngo  32702  brabsb2  32948  eqbrrdv2  32949  cmtvalN  33299  cvrval  33357  undmrnresiss  36712  cnvssco  36714  cotrintab  36723  elimaint  36742  coiun1  36746  elintima  36747  briunov2  36776  brtrclfv2  36821  frege77d  36840  dfhe3  36872  dffrege76  37036  frege97  37057  frege98  37058  frege109  37069  frege110  37070  dffrege115  37075  frege131  37091  frege133  37093  rfovcnvf1od  37101  fsovrfovd  37106  fourierdlem42  38825  ovolval2lem  39316  ovolval4lem2  39323  afveu  39666  fnopafvb  39668  tz6.12-afv  39686  tz6.12-1-afv  39687  aovprc  39701  aovrcl  39702  is1wlk  40794  isWlk  40795  1wlkcpr  40814  1wlkcomp  40816  1wlkeq  40819  1wlklenvclwlk  40844  1wlkreslem  40859  clWlkcomp  40967  1wlkpwwlkf1ouspgr  41057  wlknwwlksnsur  41068  wlkwwlksur  41075  clwlksfoclwwlk  41251  inclfusubc  41638  funcrngcsetc  41771  funcrngcsetcALT  41772  funcringcsetc  41808
  Copyright terms: Public domain W3C validator