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

Definition df-br 3921
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 8752 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 20631). Often class  R meets the  Rel criteria to be defined in df-rel 4595, and in particular  R may be a function (see df-fun 4602). 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 3920 . 2  wff  A R B
51, 2cop 3547 . . 3  class  <. A ,  B >.
65, 3wcel 1621 . 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  3922  breq1  3923  breq2  3924  ssbrd  3961  nfbrd  3963  brun  3966  brin  3967  brdif  3968  opabss  3977  brabsbOLD  4167  brabsb  4169  brabga  4172  epelg  4199  pofun  4223  brxp  4627  brab2a  4645  brab2ga  4670  eqbrriv  4689  eqbrrdv  4691  eqbrrdiv  4692  opeliunxp2  4731  opelco2g  4758  opelco  4760  cnvss  4761  elcnv2  4766  opelcnvg  4768  brcnvg  4769  dfdm3  4774  dfrn3  4776  elrng  4778  eldm2g  4782  breldm  4790  dmopab  4796  opelrn  4817  elrn  4826  rnopab  4831  brres  4868  brresg  4870  resieq  4872  opelresiOLD  4873  opelresi  4874  resiexg  4904  iss  4905  dfres2  4909  dfima3  4922  elima3  4926  imai  4934  elimasn  4945  elimasni  4947  eliniseg  4949  cotr  4962  issref  4963  cnvsym  4964  intasym  4965  asymref  4966  asymref2  4967  intirr  4968  codir  4970  qfto  4971  poirr2  4974  sofld  5028  dmsnn0  5044  coiun  5088  co02  5092  coi1  5094  dffun4  5125  dffun5  5126  funeu2  5137  funopab  5145  funcnvsn  5154  isarep1  5188  fnop  5204  fneu2  5206  fv2  5373  tz6.12  5397  funopfv  5414  fnopfvb  5416  dffv2  5444  funfvbrb  5490  dff3  5525  dff4  5526  f1ompt  5534  idref  5611  foeqcnvco  5656  f1eqcocnv  5657  fliftel  5660  fliftel1  5661  fliftcnv  5662  f1oiso  5700  ovprc  5737  1st2ndbr  6021  frxp  6077  xporderlem  6078  ottpos  6096  dftpos3  6104  dftpos4  6105  tposoprab  6122  fvopab5  6173  opabiota  6177  tfrlem9a  6288  seqomlem2  6349  seqomlem3  6350  seqomlem4  6351  0we1  6391  brwitnlem  6392  ercnv  6567  brdifun  6573  swoord1  6575  swoord2  6576  0er  6581  elecg  6584  iiner  6617  brecop  6637  brsdom  6770  brdom2  6777  idssen  6792  xpcomco  6837  omxpenlem  6848  brsdom2  6870  infxpenlem  7525  dcomex  7957  brdom3  8037  brdom7disj  8040  brdom6disj  8041  fpwwe2lem8  8139  fpwwe2lem9  8140  fpwwe2lem12  8143  canthwe  8153  dmrecnq  8472  xrlenlt  8770  climcau  12021  caucvgb  12029  divides  12407  vdwpc  12901  isstruct  13032  prdsleval  13250  imasaddfnlem  13304  imasvscafn  13313  invsym2  13509  funcf1  13584  funcixp  13585  funcid  13588  funcco  13589  funcsect  13590  funcinv  13591  funciso  13592  funcoppc  13593  idfucl  13599  cofuval2  13605  cofucl  13606  funcres  13614  funcres2b  13615  funcres2  13616  wunfunc  13617  funcpropd  13618  funcres2c  13619  isfull  13628  isfth  13632  fthsect  13643  fthinv  13644  fthmon  13645  fthepi  13646  ffthiso  13647  fthres2  13650  idffth  13651  cofull  13652  cofth  13653  ressffth  13656  isnat  13665  natixp  13670  nati  13673  elhomai2  13710  homa1  13713  homahom2  13714  eldmcoa  13741  coapm  13747  catcisolem  13782  catciso  13783  1stfcl  13815  2ndfcl  13816  prfcl  13821  evlfcl  13840  curf1cl  13846  curfcl  13850  hofcl  13877  yonedalem1  13890  yonedalem21  13891  yonedalem22  13896  yonffthlem  13900  yoniso  13903  pospo  13951  efgi  14863  efgi2  14869  gsum2d2lem  15059  dmdprd  15071  dprdval  15073  eldprd  15074  dprd2dlem2  15110  dprd2dlem1  15111  dprd2da  15112  dprd2d2  15114  isunit  15274  subrgdvds  15394  opsrtoslem2  16058  eltopspOLD  16488  tpsexOLD  16489  lmrcl  16793  lmff  16861  2ndcctbss  17013  2ndcdisj  17014  hausdiag  17171  hauseqlcld  17172  tgphaus  17631  xmeterval  17810  isphtpc  18324  ovolfcl  18658  ovollb2lem  18679  ovolctb  18681  ovolshftlem1  18700  ovolscalem1  18704  ovolicc1  18707  ioombl1lem1  18747  ioorf  18760  dyadf  18778  eldv  19080  dvres2  19094  dvef  19159  eltayl  19571  ulmscl  19590  ex-br  20631  avril1  20666  helloworld  20668  isrngo  20875  rngoablo2  20919  isdivrngo  20928  vcex  20966  h2hlm  21390  axhcompl-zf  21408  iseupa  23052  relexpindlem  23207  dfrtrclrec2  23211  rtrclreclem.trans  23214  brtpid1  23246  brtpid2  23247  brtpid3  23248  brtp  23276  dfso2  23281  dfpo2  23282  fundmpss  23290  elpredim  23344  elpredg  23346  wfrlem11  23434  frrlem5c  23455  brsymdif  23547  brv  23592  pprodss4v  23599  brsset  23604  brtxpsd  23609  brimg  23650  funpartfun  23655  funpartfv  23657  dfrdg4  23662  brbtwn  23701  fvtransport  23829  brcolinear2  23855  colineardim1  23858  fvray  23938  fvline  23941  restidsing  24241  prj1b  24244  prj3  24245  domintrefc  24291  deref  24454  dfdir2  24457  vecval1b  24617  glmrngo  24648  bosser  25333  eltail  25489  heiborlem3  25703  heiborlem4  25704  heiborlem6  25706  brabsb2  25896  eqbrrdv2  25897  cmtvalN  28090  cvrval  28148
  Copyright terms: Public domain W3C validator