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

Definition df-br 4216
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  R often denotes a relation such as " < " that compares two classes  A and 
B, which might be numbers such as  1 and  2 (see df-ltxr 9130 for the specific definition of  <). As a wff, relations are true or false. For example,  ( R  =  { <. 2 ,  6
>. ,  <. 3 ,  9 >. }  ->  3 R 9 ) (ex-br 21744). Often class  R meets the  Rel criteria to be defined in df-rel 4888, and in particular  R may be a function (see df-fun 5459). This definition of relations is well-defined, although not very meaningful, when classes  A and/or  B are proper classes (i.e. are not sets). On the other hand, we often find uses for this definition when  R is a proper class. (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
df-br  |-  ( A R B  <->  <. A ,  B >.  e.  R )

Detailed syntax breakdown of Definition df-br
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cR . . 3  class  R
41, 2, 3wbr 4215 . 2  wff  A R B
51, 2cop 3819 . . 3  class  <. A ,  B >.
65, 3wcel 1726 . 2  wff  <. A ,  B >.  e.  R
74, 6wb 178 1  wff  ( A R B  <->  <. A ,  B >.  e.  R )
Colors of variables: wff set class
This definition is referenced by:  breq  4217  breq1  4218  breq2  4219  ssbrd  4256  nfbrd  4258  brun  4261  brin  4262  brdif  4263  opabss  4272  brabsbOLD  4467  brabsb  4469  brabga  4472  epelg  4498  pofun  4522  brxp  4912  brab2a  4930  brab2ga  4954  eqbrriv  4974  eqbrrdv  4976  eqbrrdiv  4977  opeliunxp2  5016  opelco2g  5043  opelco  5047  cnvss  5048  elcnv2  5053  opelcnvg  5055  brcnvg  5056  dfdm3  5061  dfrn3  5063  elrng  5065  eldm2g  5069  breldm  5077  dmopab  5083  opelrn  5104  elrn  5113  rnopab  5118  brres  5155  brresg  5157  resieq  5159  opelresiOLD  5160  opelresi  5161  resiexg  5191  iss  5192  dfres2  5196  dfima3  5209  elima3  5213  imai  5221  elimasn  5232  elimasni  5234  eliniseg  5236  cotr  5249  issref  5250  cnvsym  5251  intasym  5252  asymref  5253  asymref2  5254  intirr  5255  codir  5257  qfto  5258  poirr2  5261  sofld  5321  dmsnn0  5338  coiun  5382  co02  5386  coi1  5388  dffun4  5469  dffun5  5470  funeu2  5481  funopab  5489  funcnvsn  5499  isarep1  5535  fnop  5551  fneu2  5553  brprcneu  5724  dffv3  5727  tz6.12  5751  funopfv  5769  fnopfvb  5771  dffv2  5799  funfvbrb  5846  dff3  5885  dff4  5886  f1ompt  5894  idref  5982  foeqcnvco  6030  f1eqcocnv  6031  fliftel  6034  fliftel1  6035  fliftcnv  6036  f1oiso  6074  ovprc  6111  brabv  6123  1st2ndbr  6399  bropopvvv  6429  frxp  6459  xporderlem  6460  brovex  6477  isprmpt2  6480  ottpos  6492  dftpos3  6500  dftpos4  6501  tposoprab  6518  fvopab5  6537  opabiota  6541  tfrlem9a  6650  seqomlem2  6711  seqomlem3  6712  seqomlem4  6713  0we1  6753  brwitnlem  6754  ercnv  6929  brdifun  6935  swoord1  6937  swoord2  6938  0er  6943  elecg  6946  iiner  6979  brecop  7000  brsdom  7133  brdom2  7140  idssen  7155  xpcomco  7201  omxpenlem  7212  brsdom2  7234  infxpenlem  7900  dcomex  8332  brdom3  8411  brdom7disj  8414  brdom6disj  8415  fpwwe2lem8  8517  fpwwe2lem9  8518  fpwwe2lem12  8521  canthwe  8531  dmrecnq  8850  xrlenlt  9148  climcau  12469  caucvgb  12478  divides  12859  vdwpc  13353  isstruct  13484  prdsleval  13704  imasaddfnlem  13758  imasvscafn  13767  invsym2  13993  funcf1  14068  funcixp  14069  funcid  14072  funcco  14073  funcsect  14074  funcinv  14075  funciso  14076  funcoppc  14077  idfucl  14083  cofuval2  14089  cofucl  14090  funcres  14098  funcres2b  14099  funcres2  14100  wunfunc  14101  funcpropd  14102  funcres2c  14103  isfull  14112  isfth  14116  fthsect  14127  fthinv  14128  fthmon  14129  fthepi  14130  ffthiso  14131  fthres2  14134  idffth  14135  cofull  14136  cofth  14137  ressffth  14140  isnat  14149  natixp  14154  nati  14157  elhomai2  14194  homa1  14197  homahom2  14198  eldmcoa  14225  coapm  14231  catcisolem  14266  catciso  14267  1stfcl  14299  2ndfcl  14300  prfcl  14305  evlfcl  14324  curf1cl  14330  curfcl  14334  hofcl  14361  yonedalem1  14374  yonedalem21  14375  yonedalem22  14380  yonffthlem  14384  yoniso  14387  pospo  14435  efgi  15356  efgi2  15362  gsum2d2lem  15552  dmdprd  15564  dprdval  15566  eldprd  15567  dprd2dlem2  15603  dprd2dlem1  15604  dprd2da  15605  dprd2d2  15607  isunit  15767  subrgdvds  15887  opsrtoslem2  16550  eltopspOLD  16988  tpsexOLD  16989  lmrcl  17300  lmff  17370  2ndcctbss  17523  2ndcdisj  17524  hausdiag  17682  hauseqlcld  17683  cnextfun  18100  cnextfvval  18101  tgphaus  18151  utop2nei  18285  utop3cls  18286  ucnima  18316  xmeterval  18467  metustidOLD  18594  metustid  18595  metustsymOLD  18596  metustsym  18597  metustexhalfOLD  18598  metustexhalf  18599  elbl4  18611  metuel2  18614  isphtpc  19024  ovolfcl  19368  ovollb2lem  19389  ovolctb  19391  ovolshftlem1  19410  ovolscalem1  19414  ovolicc1  19417  ioombl1lem1  19457  ioorf  19470  dyadf  19488  eldv  19790  dvres2  19804  dvef  19869  eltayl  20281  ulmscl  20300  iswlk  21532  istrl  21542  ispth  21573  isspth  21574  ex-br  21744  avril1  21762  helloworld  21764  isrngo  21971  rngoablo2  22015  isdivrngo  22024  vcex  22064  h2hlm  22488  axhcompl-zf  22506  isarchi  24257  relexpindlem  25144  dfrtrclrec2  25148  rtrclreclem.trans  25151  brtpid1  25183  brtpid2  25184  brtpid3  25185  brtp  25377  dfso2  25382  dfpo2  25383  fundmpss  25395  opelco3  25408  elpredim  25456  elpredg  25458  wfrlem11  25553  frrlem5c  25593  brsymdif  25678  brv  25727  pprodss4v  25734  brsset  25739  brtxpsd  25744  sscoid  25763  dffun10  25764  brimg  25787  funpartfun  25793  funpartfv  25795  dfrdg4  25800  imagesset  25803  brbtwn  25843  fvtransport  25971  brcolinear2  25997  colineardim1  26000  fvray  26080  fvline  26083  mblfinlem2  26256  areacirclem5  26310  eltail  26417  heiborlem3  26536  heiborlem4  26537  heiborlem6  26539  brabsb2  26725  eqbrrdv2  26726  afveu  28007  fnopafvb  28009  tz6.12-afv  28027  tz6.12-1-afv  28028  aovprc  28042  aovrcl  28043  breqn0  28084  oprabv  28103  wlkcomp  28339  2wlkeq  28341  isrgra  28441  isrusgra  28442  cmtvalN  30083  cvrval  30141
  Copyright terms: Public domain W3C validator