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

Definition df-br 4173
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 9081 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 21692). Often class  R meets the  Rel criteria to be defined in df-rel 4844, and in particular  R may be a function (see df-fun 5415). 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 4172 . 2  wff  A R B
51, 2cop 3777 . . 3  class  <. A ,  B >.
65, 3wcel 1721 . 2  wff  <. A ,  B >.  e.  R
74, 6wb 177 1  wff  ( A R B  <->  <. A ,  B >.  e.  R )
Colors of variables: wff set class
This definition is referenced by:  breq  4174  breq1  4175  breq2  4176  ssbrd  4213  nfbrd  4215  brun  4218  brin  4219  brdif  4220  opabss  4229  brabsbOLD  4424  brabsb  4426  brabga  4429  epelg  4455  pofun  4479  brxp  4868  brab2a  4886  brab2ga  4910  eqbrriv  4930  eqbrrdv  4932  eqbrrdiv  4933  opeliunxp2  4972  opelco2g  4999  opelco  5003  cnvss  5004  elcnv2  5009  opelcnvg  5011  brcnvg  5012  dfdm3  5017  dfrn3  5019  elrng  5021  eldm2g  5025  breldm  5033  dmopab  5039  opelrn  5060  elrn  5069  rnopab  5074  brres  5111  brresg  5113  resieq  5115  opelresiOLD  5116  opelresi  5117  resiexg  5147  iss  5148  dfres2  5152  dfima3  5165  elima3  5169  imai  5177  elimasn  5188  elimasni  5190  eliniseg  5192  cotr  5205  issref  5206  cnvsym  5207  intasym  5208  asymref  5209  asymref2  5210  intirr  5211  codir  5213  qfto  5214  poirr2  5217  sofld  5277  dmsnn0  5294  coiun  5338  co02  5342  coi1  5344  dffun4  5425  dffun5  5426  funeu2  5437  funopab  5445  funcnvsn  5455  isarep1  5491  fnop  5507  fneu2  5509  brprcneu  5680  dffv3  5683  tz6.12  5707  funopfv  5725  fnopfvb  5727  dffv2  5755  funfvbrb  5802  dff3  5841  dff4  5842  f1ompt  5850  idref  5938  foeqcnvco  5986  f1eqcocnv  5987  fliftel  5990  fliftel1  5991  fliftcnv  5992  f1oiso  6030  ovprc  6067  brabv  6079  1st2ndbr  6355  bropopvvv  6385  frxp  6415  xporderlem  6416  brovex  6433  isprmpt2  6436  ottpos  6448  dftpos3  6456  dftpos4  6457  tposoprab  6474  fvopab5  6493  opabiota  6497  tfrlem9a  6606  seqomlem2  6667  seqomlem3  6668  seqomlem4  6669  0we1  6709  brwitnlem  6710  ercnv  6885  brdifun  6891  swoord1  6893  swoord2  6894  0er  6899  elecg  6902  iiner  6935  brecop  6956  brsdom  7089  brdom2  7096  idssen  7111  xpcomco  7157  omxpenlem  7168  brsdom2  7190  infxpenlem  7851  dcomex  8283  brdom3  8362  brdom7disj  8365  brdom6disj  8366  fpwwe2lem8  8468  fpwwe2lem9  8469  fpwwe2lem12  8472  canthwe  8482  dmrecnq  8801  xrlenlt  9099  climcau  12419  caucvgb  12428  divides  12809  vdwpc  13303  isstruct  13434  prdsleval  13654  imasaddfnlem  13708  imasvscafn  13717  invsym2  13943  funcf1  14018  funcixp  14019  funcid  14022  funcco  14023  funcsect  14024  funcinv  14025  funciso  14026  funcoppc  14027  idfucl  14033  cofuval2  14039  cofucl  14040  funcres  14048  funcres2b  14049  funcres2  14050  wunfunc  14051  funcpropd  14052  funcres2c  14053  isfull  14062  isfth  14066  fthsect  14077  fthinv  14078  fthmon  14079  fthepi  14080  ffthiso  14081  fthres2  14084  idffth  14085  cofull  14086  cofth  14087  ressffth  14090  isnat  14099  natixp  14104  nati  14107  elhomai2  14144  homa1  14147  homahom2  14148  eldmcoa  14175  coapm  14181  catcisolem  14216  catciso  14217  1stfcl  14249  2ndfcl  14250  prfcl  14255  evlfcl  14274  curf1cl  14280  curfcl  14284  hofcl  14311  yonedalem1  14324  yonedalem21  14325  yonedalem22  14330  yonffthlem  14334  yoniso  14337  pospo  14385  efgi  15306  efgi2  15312  gsum2d2lem  15502  dmdprd  15514  dprdval  15516  eldprd  15517  dprd2dlem2  15553  dprd2dlem1  15554  dprd2da  15555  dprd2d2  15557  isunit  15717  subrgdvds  15837  opsrtoslem2  16500  eltopspOLD  16938  tpsexOLD  16939  lmrcl  17249  lmff  17319  2ndcctbss  17471  2ndcdisj  17472  hausdiag  17630  hauseqlcld  17631  cnextfun  18048  cnextfvval  18049  tgphaus  18099  utop2nei  18233  utop3cls  18234  ucnima  18264  xmeterval  18415  metustidOLD  18542  metustid  18543  metustsymOLD  18544  metustsym  18545  metustexhalfOLD  18546  metustexhalf  18547  elbl4  18559  metuel2  18562  isphtpc  18972  ovolfcl  19316  ovollb2lem  19337  ovolctb  19339  ovolshftlem1  19358  ovolscalem1  19362  ovolicc1  19365  ioombl1lem1  19405  ioorf  19418  dyadf  19436  eldv  19738  dvres2  19752  dvef  19817  eltayl  20229  ulmscl  20248  iswlk  21480  istrl  21490  ispth  21521  isspth  21522  ex-br  21692  avril1  21710  helloworld  21712  isrngo  21919  rngoablo2  21963  isdivrngo  21972  vcex  22012  h2hlm  22436  axhcompl-zf  22454  isarchi  24205  relexpindlem  25092  dfrtrclrec2  25096  rtrclreclem.trans  25099  brtpid1  25131  brtpid2  25132  brtpid3  25133  brtp  25320  dfso2  25325  dfpo2  25326  fundmpss  25336  elpredim  25390  elpredg  25392  wfrlem11  25480  frrlem5c  25501  brsymdif  25586  brv  25631  pprodss4v  25638  brsset  25643  brtxpsd  25648  dffun10  25667  brimg  25690  funpartfun  25696  funpartfv  25698  dfrdg4  25703  brbtwn  25742  fvtransport  25870  brcolinear2  25896  colineardim1  25899  fvray  25979  fvline  25982  mblfinlem  26143  areacirclem6  26186  eltail  26293  heiborlem3  26412  heiborlem4  26413  heiborlem6  26415  brabsb2  26601  eqbrrdv2  26602  afveu  27884  fnopafvb  27886  tz6.12-afv  27904  tz6.12-1-afv  27905  aovprc  27919  aovrcl  27920  cmtvalN  29694  cvrval  29752
  Copyright terms: Public domain W3C validator