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

Definition df-br 4040
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 8888 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 20834). Often class  R meets the  Rel criteria to be defined in df-rel 4712, and in particular  R may be a function (see df-fun 5273). 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 4039 . 2  wff  A R B
51, 2cop 3656 . . 3  class  <. A ,  B >.
65, 3wcel 1696 . 2  wff  <. A ,  B >.  e.  R
74, 6wb 176 1  wff  ( A R B  <->  <. A ,  B >.  e.  R )
Colors of variables: wff set class
This definition is referenced by:  breq  4041  breq1  4042  breq2  4043  ssbrd  4080  nfbrd  4082  brun  4085  brin  4086  brdif  4087  opabss  4096  brabsbOLD  4290  brabsb  4292  brabga  4295  epelg  4322  pofun  4346  brxp  4736  brab2a  4754  brab2ga  4779  eqbrriv  4798  eqbrrdv  4800  eqbrrdiv  4801  opeliunxp2  4840  opelco2g  4867  opelco  4869  cnvss  4870  elcnv2  4875  opelcnvg  4877  brcnvg  4878  dfdm3  4883  dfrn3  4885  elrng  4887  eldm2g  4891  breldm  4899  dmopab  4905  opelrn  4926  elrn  4935  rnopab  4940  brres  4977  brresg  4979  resieq  4981  opelresiOLD  4982  opelresi  4983  resiexg  5013  iss  5014  dfres2  5018  dfima3  5031  elima3  5035  imai  5043  elimasn  5054  elimasni  5056  eliniseg  5058  cotr  5071  issref  5072  cnvsym  5073  intasym  5074  asymref  5075  asymref2  5076  intirr  5077  codir  5079  qfto  5080  poirr2  5083  sofld  5137  dmsnn0  5154  coiun  5198  co02  5202  coi1  5204  dffun4  5283  dffun5  5284  funeu2  5295  funopab  5303  funcnvsn  5313  isarep1  5347  fnop  5363  fneu2  5365  brprcneu  5534  dffv3  5537  tz6.12  5561  funopfv  5578  fnopfvb  5580  dffv2  5608  funfvbrb  5654  dff3  5689  dff4  5690  f1ompt  5698  idref  5775  foeqcnvco  5820  f1eqcocnv  5821  fliftel  5824  fliftel1  5825  fliftcnv  5826  f1oiso  5864  ovprc  5901  1st2ndbr  6185  frxp  6241  xporderlem  6242  ottpos  6260  dftpos3  6268  dftpos4  6269  tposoprab  6286  fvopab5  6305  opabiota  6309  tfrlem9a  6418  seqomlem2  6479  seqomlem3  6480  seqomlem4  6481  0we1  6521  brwitnlem  6522  ercnv  6697  brdifun  6703  swoord1  6705  swoord2  6706  0er  6711  elecg  6714  iiner  6747  brecop  6767  brsdom  6900  brdom2  6907  idssen  6922  xpcomco  6968  omxpenlem  6979  brsdom2  7001  infxpenlem  7657  dcomex  8089  brdom3  8169  brdom7disj  8172  brdom6disj  8173  fpwwe2lem8  8275  fpwwe2lem9  8276  fpwwe2lem12  8279  canthwe  8289  dmrecnq  8608  xrlenlt  8906  climcau  12160  caucvgb  12168  divides  12549  vdwpc  13043  isstruct  13174  prdsleval  13392  imasaddfnlem  13446  imasvscafn  13455  invsym2  13681  funcf1  13756  funcixp  13757  funcid  13760  funcco  13761  funcsect  13762  funcinv  13763  funciso  13764  funcoppc  13765  idfucl  13771  cofuval2  13777  cofucl  13778  funcres  13786  funcres2b  13787  funcres2  13788  wunfunc  13789  funcpropd  13790  funcres2c  13791  isfull  13800  isfth  13804  fthsect  13815  fthinv  13816  fthmon  13817  fthepi  13818  ffthiso  13819  fthres2  13822  idffth  13823  cofull  13824  cofth  13825  ressffth  13828  isnat  13837  natixp  13842  nati  13845  elhomai2  13882  homa1  13885  homahom2  13886  eldmcoa  13913  coapm  13919  catcisolem  13954  catciso  13955  1stfcl  13987  2ndfcl  13988  prfcl  13993  evlfcl  14012  curf1cl  14018  curfcl  14022  hofcl  14049  yonedalem1  14062  yonedalem21  14063  yonedalem22  14068  yonffthlem  14072  yoniso  14075  pospo  14123  efgi  15044  efgi2  15050  gsum2d2lem  15240  dmdprd  15252  dprdval  15254  eldprd  15255  dprd2dlem2  15291  dprd2dlem1  15292  dprd2da  15293  dprd2d2  15295  isunit  15455  subrgdvds  15575  opsrtoslem2  16242  eltopspOLD  16672  tpsexOLD  16673  lmrcl  16977  lmff  17045  2ndcctbss  17197  2ndcdisj  17198  hausdiag  17355  hauseqlcld  17356  tgphaus  17815  xmeterval  17994  isphtpc  18508  ovolfcl  18842  ovollb2lem  18863  ovolctb  18865  ovolshftlem1  18884  ovolscalem1  18888  ovolicc1  18891  ioombl1lem1  18931  ioorf  18944  dyadf  18962  eldv  19264  dvres2  19278  dvef  19343  eltayl  19755  ulmscl  19774  ex-br  20834  avril1  20852  helloworld  20854  isrngo  21061  rngoablo2  21105  isdivrngo  21114  vcex  21152  h2hlm  21576  axhcompl-zf  21594  iseupa  23896  relexpindlem  24051  dfrtrclrec2  24055  rtrclreclem.trans  24058  brtpid1  24090  brtpid2  24091  brtpid3  24092  brtp  24177  dfso2  24182  dfpo2  24183  fundmpss  24193  elpredim  24247  elpredg  24249  wfrlem11  24337  frrlem5c  24358  brsymdif  24443  brv  24488  pprodss4v  24495  brsset  24500  brtxpsd  24505  dffun10  24524  brimg  24547  funpartfun  24553  funpartfv  24555  dfrdg4  24560  brbtwn  24599  fvtransport  24727  brcolinear2  24753  colineardim1  24756  fvray  24836  fvline  24839  areacirclem6  25033  restidsing  25179  prj1b  25182  prj3  25183  domintrefc  25228  deref  25391  dfdir2  25394  vecval1b  25554  glmrngo  25585  bosser  26270  eltail  26426  heiborlem3  26640  heiborlem4  26641  heiborlem6  26643  brabsb2  26833  eqbrrdv2  26834  afveu  28121  fnopafvb  28123  tz6.12-afv  28141  tz6.12-1-afv  28142  aovprc  28156  aovrcl  28157  brabv  28193  brovex  28205  isprmpt2  28208  iswlk  28329  istrl  28336  trlonprop  28341  ispth  28354  isspth  28355  cmtvalN  30023  cvrval  30081
  Copyright terms: Public domain W3C validator