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

Definition df-br 4213
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 9125 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 21739). Often class  R meets the  Rel criteria to be defined in df-rel 4885, and in particular  R may be a function (see df-fun 5456). 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 4212 . 2  wff  A R B
51, 2cop 3817 . . 3  class  <. A ,  B >.
65, 3wcel 1725 . 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  4214  breq1  4215  breq2  4216  ssbrd  4253  nfbrd  4255  brun  4258  brin  4259  brdif  4260  opabss  4269  brabsbOLD  4464  brabsb  4466  brabga  4469  epelg  4495  pofun  4519  brxp  4909  brab2a  4927  brab2ga  4951  eqbrriv  4971  eqbrrdv  4973  eqbrrdiv  4974  opeliunxp2  5013  opelco2g  5040  opelco  5044  cnvss  5045  elcnv2  5050  opelcnvg  5052  brcnvg  5053  dfdm3  5058  dfrn3  5060  elrng  5062  eldm2g  5066  breldm  5074  dmopab  5080  opelrn  5101  elrn  5110  rnopab  5115  brres  5152  brresg  5154  resieq  5156  opelresiOLD  5157  opelresi  5158  resiexg  5188  iss  5189  dfres2  5193  dfima3  5206  elima3  5210  imai  5218  elimasn  5229  elimasni  5231  eliniseg  5233  cotr  5246  issref  5247  cnvsym  5248  intasym  5249  asymref  5250  asymref2  5251  intirr  5252  codir  5254  qfto  5255  poirr2  5258  sofld  5318  dmsnn0  5335  coiun  5379  co02  5383  coi1  5385  dffun4  5466  dffun5  5467  funeu2  5478  funopab  5486  funcnvsn  5496  isarep1  5532  fnop  5548  fneu2  5550  brprcneu  5721  dffv3  5724  tz6.12  5748  funopfv  5766  fnopfvb  5768  dffv2  5796  funfvbrb  5843  dff3  5882  dff4  5883  f1ompt  5891  idref  5979  foeqcnvco  6027  f1eqcocnv  6028  fliftel  6031  fliftel1  6032  fliftcnv  6033  f1oiso  6071  ovprc  6108  brabv  6120  1st2ndbr  6396  bropopvvv  6426  frxp  6456  xporderlem  6457  brovex  6474  isprmpt2  6477  ottpos  6489  dftpos3  6497  dftpos4  6498  tposoprab  6515  fvopab5  6534  opabiota  6538  tfrlem9a  6647  seqomlem2  6708  seqomlem3  6709  seqomlem4  6710  0we1  6750  brwitnlem  6751  ercnv  6926  brdifun  6932  swoord1  6934  swoord2  6935  0er  6940  elecg  6943  iiner  6976  brecop  6997  brsdom  7130  brdom2  7137  idssen  7152  xpcomco  7198  omxpenlem  7209  brsdom2  7231  infxpenlem  7895  dcomex  8327  brdom3  8406  brdom7disj  8409  brdom6disj  8410  fpwwe2lem8  8512  fpwwe2lem9  8513  fpwwe2lem12  8516  canthwe  8526  dmrecnq  8845  xrlenlt  9143  climcau  12464  caucvgb  12473  divides  12854  vdwpc  13348  isstruct  13479  prdsleval  13699  imasaddfnlem  13753  imasvscafn  13762  invsym2  13988  funcf1  14063  funcixp  14064  funcid  14067  funcco  14068  funcsect  14069  funcinv  14070  funciso  14071  funcoppc  14072  idfucl  14078  cofuval2  14084  cofucl  14085  funcres  14093  funcres2b  14094  funcres2  14095  wunfunc  14096  funcpropd  14097  funcres2c  14098  isfull  14107  isfth  14111  fthsect  14122  fthinv  14123  fthmon  14124  fthepi  14125  ffthiso  14126  fthres2  14129  idffth  14130  cofull  14131  cofth  14132  ressffth  14135  isnat  14144  natixp  14149  nati  14152  elhomai2  14189  homa1  14192  homahom2  14193  eldmcoa  14220  coapm  14226  catcisolem  14261  catciso  14262  1stfcl  14294  2ndfcl  14295  prfcl  14300  evlfcl  14319  curf1cl  14325  curfcl  14329  hofcl  14356  yonedalem1  14369  yonedalem21  14370  yonedalem22  14375  yonffthlem  14379  yoniso  14382  pospo  14430  efgi  15351  efgi2  15357  gsum2d2lem  15547  dmdprd  15559  dprdval  15561  eldprd  15562  dprd2dlem2  15598  dprd2dlem1  15599  dprd2da  15600  dprd2d2  15602  isunit  15762  subrgdvds  15882  opsrtoslem2  16545  eltopspOLD  16983  tpsexOLD  16984  lmrcl  17295  lmff  17365  2ndcctbss  17518  2ndcdisj  17519  hausdiag  17677  hauseqlcld  17678  cnextfun  18095  cnextfvval  18096  tgphaus  18146  utop2nei  18280  utop3cls  18281  ucnima  18311  xmeterval  18462  metustidOLD  18589  metustid  18590  metustsymOLD  18591  metustsym  18592  metustexhalfOLD  18593  metustexhalf  18594  elbl4  18606  metuel2  18609  isphtpc  19019  ovolfcl  19363  ovollb2lem  19384  ovolctb  19386  ovolshftlem1  19405  ovolscalem1  19409  ovolicc1  19412  ioombl1lem1  19452  ioorf  19465  dyadf  19483  eldv  19785  dvres2  19799  dvef  19864  eltayl  20276  ulmscl  20295  iswlk  21527  istrl  21537  ispth  21568  isspth  21569  ex-br  21739  avril1  21757  helloworld  21759  isrngo  21966  rngoablo2  22010  isdivrngo  22019  vcex  22059  h2hlm  22483  axhcompl-zf  22501  isarchi  24252  relexpindlem  25139  dfrtrclrec2  25143  rtrclreclem.trans  25146  brtpid1  25178  brtpid2  25179  brtpid3  25180  brtp  25372  dfso2  25377  dfpo2  25378  fundmpss  25390  opelco3  25403  elpredim  25451  elpredg  25453  wfrlem11  25548  frrlem5c  25588  brsymdif  25673  brv  25722  pprodss4v  25729  brsset  25734  brtxpsd  25739  sscoid  25758  dffun10  25759  brimg  25782  funpartfun  25788  funpartfv  25790  dfrdg4  25795  imagesset  25798  brbtwn  25838  fvtransport  25966  brcolinear2  25992  colineardim1  25995  fvray  26075  fvline  26078  mblfinlem2  26244  areacirclem5  26296  eltail  26403  heiborlem3  26522  heiborlem4  26523  heiborlem6  26525  brabsb2  26711  eqbrrdv2  26712  afveu  27993  fnopafvb  27995  tz6.12-afv  28013  tz6.12-1-afv  28014  aovprc  28028  aovrcl  28029  breqn0  28069  oprabv  28085  wlkcomp  28301  2wlkeq  28303  isrgra  28369  isrusgra  28370  cmtvalN  30009  cvrval  30067
  Copyright terms: Public domain W3C validator