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

Definition df-br 4027
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 8869 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 20795). Often class  R meets the  Rel criteria to be defined in df-rel 4697, and in particular  R may be a function (see df-fun 5225). 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 4026 . 2  wff  A R B
51, 2cop 3646 . . 3  class  <. A ,  B >.
65, 3wcel 1687 . 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  4028  breq1  4029  breq2  4030  ssbrd  4067  nfbrd  4069  brun  4072  brin  4073  brdif  4074  opabss  4083  brabsbOLD  4275  brabsb  4277  brabga  4280  epelg  4307  pofun  4331  brxp  4721  brab2a  4739  brab2ga  4764  eqbrriv  4783  eqbrrdv  4785  eqbrrdiv  4786  opeliunxp2  4825  opelco2g  4852  opelco  4854  cnvss  4855  elcnv2  4860  opelcnvg  4862  brcnvg  4863  dfdm3  4868  dfrn3  4870  elrng  4872  eldm2g  4876  breldm  4884  dmopab  4890  opelrn  4911  elrn  4920  rnopab  4925  brres  4962  brresg  4964  resieq  4966  opelresiOLD  4967  opelresi  4968  resiexg  4998  iss  4999  dfres2  5003  dfima3  5016  elima3  5020  imai  5028  elimasn  5039  elimasni  5041  eliniseg  5043  cotr  5056  issref  5057  cnvsym  5058  intasym  5059  asymref  5060  asymref2  5061  intirr  5062  codir  5064  qfto  5065  poirr2  5068  sofld  5122  dmsnn0  5138  coiun  5182  co02  5186  coi1  5188  dffun4  5235  dffun5  5236  funeu2  5247  funopab  5255  funcnvsn  5264  isarep1  5298  fnop  5314  fneu2  5316  fv2  5483  tz6.12  5507  funopfv  5525  fnopfvb  5527  dffv2  5555  funfvbrb  5601  dff3  5636  dff4  5637  f1ompt  5645  idref  5722  foeqcnvco  5767  f1eqcocnv  5768  fliftel  5771  fliftel1  5772  fliftcnv  5773  f1oiso  5811  ovprc  5848  1st2ndbr  6132  frxp  6188  xporderlem  6189  ottpos  6207  dftpos3  6215  dftpos4  6216  tposoprab  6233  fvopab5  6284  opabiota  6288  tfrlem9a  6399  seqomlem2  6460  seqomlem3  6461  seqomlem4  6462  0we1  6502  brwitnlem  6503  ercnv  6678  brdifun  6684  swoord1  6686  swoord2  6687  0er  6692  elecg  6695  iiner  6728  brecop  6748  brsdom  6881  brdom2  6888  idssen  6903  xpcomco  6949  omxpenlem  6960  brsdom2  6982  infxpenlem  7638  dcomex  8070  brdom3  8150  brdom7disj  8153  brdom6disj  8154  fpwwe2lem8  8256  fpwwe2lem9  8257  fpwwe2lem12  8260  canthwe  8270  dmrecnq  8589  xrlenlt  8887  climcau  12140  caucvgb  12148  divides  12529  vdwpc  13023  isstruct  13154  prdsleval  13372  imasaddfnlem  13426  imasvscafn  13435  invsym2  13661  funcf1  13736  funcixp  13737  funcid  13740  funcco  13741  funcsect  13742  funcinv  13743  funciso  13744  funcoppc  13745  idfucl  13751  cofuval2  13757  cofucl  13758  funcres  13766  funcres2b  13767  funcres2  13768  wunfunc  13769  funcpropd  13770  funcres2c  13771  isfull  13780  isfth  13784  fthsect  13795  fthinv  13796  fthmon  13797  fthepi  13798  ffthiso  13799  fthres2  13802  idffth  13803  cofull  13804  cofth  13805  ressffth  13808  isnat  13817  natixp  13822  nati  13825  elhomai2  13862  homa1  13865  homahom2  13866  eldmcoa  13893  coapm  13899  catcisolem  13934  catciso  13935  1stfcl  13967  2ndfcl  13968  prfcl  13973  evlfcl  13992  curf1cl  13998  curfcl  14002  hofcl  14029  yonedalem1  14042  yonedalem21  14043  yonedalem22  14048  yonffthlem  14052  yoniso  14055  pospo  14103  efgi  15024  efgi2  15030  gsum2d2lem  15220  dmdprd  15232  dprdval  15234  eldprd  15235  dprd2dlem2  15271  dprd2dlem1  15272  dprd2da  15273  dprd2d2  15275  isunit  15435  subrgdvds  15555  opsrtoslem2  16222  eltopspOLD  16652  tpsexOLD  16653  lmrcl  16957  lmff  17025  2ndcctbss  17177  2ndcdisj  17178  hausdiag  17335  hauseqlcld  17336  tgphaus  17795  xmeterval  17974  isphtpc  18488  ovolfcl  18822  ovollb2lem  18843  ovolctb  18845  ovolshftlem1  18864  ovolscalem1  18868  ovolicc1  18871  ioombl1lem1  18911  ioorf  18924  dyadf  18942  eldv  19244  dvres2  19258  dvef  19323  eltayl  19735  ulmscl  19754  ex-br  20795  avril1  20830  helloworld  20832  isrngo  21039  rngoablo2  21083  isdivrngo  21092  vcex  21130  h2hlm  21554  axhcompl-zf  21572  iseupa  23287  relexpindlem  23442  dfrtrclrec2  23446  rtrclreclem.trans  23449  brtpid1  23481  brtpid2  23482  brtpid3  23483  brtp  23511  dfso2  23516  dfpo2  23517  fundmpss  23525  elpredim  23579  elpredg  23581  wfrlem11  23669  frrlem5c  23690  brsymdif  23782  brv  23827  pprodss4v  23834  brsset  23839  brtxpsd  23844  brimg  23885  funpartfun  23890  funpartfv  23892  dfrdg4  23897  brbtwn  23936  fvtransport  24064  brcolinear2  24090  colineardim1  24093  fvray  24173  fvline  24176  restidsing  24476  prj1b  24479  prj3  24480  domintrefc  24526  deref  24689  dfdir2  24692  vecval1b  24852  glmrngo  24883  bosser  25568  eltail  25724  heiborlem3  25938  heiborlem4  25939  heiborlem6  25941  brabsb2  26131  eqbrrdv2  26132  fnopafvb  27398  aovprc  27429  aovrcl  27430  cmtvalN  28670  cvrval  28728
  Copyright terms: Public domain W3C validator