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

Definition df-br 4443
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 9624 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 24817). Often class  R meets the  Rel criteria to be defined in df-rel 5001, and in particular  R may be a function (see df-fun 5583). 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 (see for example iprc 6711). (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 4442 . 2  wff  A R B
51, 2cop 4028 . . 3  class  <. A ,  B >.
65, 3wcel 1762 . 2  wff  <. A ,  B >.  e.  R
74, 6wb 184 1  wff  ( A R B  <->  <. A ,  B >.  e.  R )
Colors of variables: wff setvar class
This definition is referenced by:  breq  4444  breq1  4445  breq2  4446  ssbrd  4483  nfbrd  4485  br0  4488  brne0  4489  brun  4490  brin  4491  brdif  4492  sbcbr123  4493  opabss  4503  brabsb  4753  brabga  4756  epelg  4787  pofun  4811  brxp  5024  brab2a  5043  brab2ga  5068  eqbrriv  5091  eqbrrdv  5093  eqbrrdiv  5094  opeliunxp2  5134  opelco2g  5163  opelco  5167  cnvss  5168  elcnv2  5173  opelcnvg  5175  brcnvg  5176  dfdm3  5183  dfrn3  5185  elrng  5187  eldm2g  5192  breldm  5200  dmopab  5206  opelrn  5227  elrn  5236  rnopab  5240  brres  5273  brresg  5275  resieq  5277  opelresi  5278  iss  5314  dfres2  5319  restidsing  5323  dfima3  5333  elima3  5337  imai  5342  elimasn  5355  elimasni  5357  eliniseg  5359  cotrg  5371  issref  5373  cnvsym  5374  intasym  5375  asymref  5376  asymref2  5377  intirr  5378  codir  5380  qfto  5381  poirr2  5384  xpdifid  5428  sofld  5448  dmsnn0  5466  coiun  5510  co02  5514  coi1  5516  dffun4  5593  dffun5  5594  funeu2  5606  funopab  5614  funcnvsn  5626  isarep1  5660  fnop  5677  fneu2  5679  brprcneu  5852  dffv3  5855  tz6.12  5876  funopfv  5900  fnopfvb  5902  opabiota  5923  dffv2  5933  fvopab5  5966  funfvbrb  5987  dff3  6027  dff4  6028  f1ompt  6036  idref  6134  foeqcnvco  6184  f1eqcocnv  6185  fliftel  6188  fliftel1  6189  fliftcnv  6190  f1oiso  6228  ovprc  6304  brabv  6319  oprabv  6322  elrnmpt2res  6393  resiexg  6712  1st2ndbr  6825  bropopvvv  6855  frxp  6885  xporderlem  6886  cnvimadfsn  6902  brovex  6942  isprmpt2  6945  ottpos  6957  dftpos3  6965  dftpos4  6966  tposoprab  6983  tfrlem7  7044  tfrlem9a  7047  seqomlem2  7108  seqomlem3  7109  seqomlem4  7110  0we1  7148  brwitnlem  7149  ercnv  7324  brdifun  7330  swoord1  7332  swoord2  7333  0er  7338  elecg  7342  iiner  7375  brecop  7396  brsdom  7530  brdom2  7537  idssen  7552  xpcomco  7599  omxpenlem  7610  brsdom2  7633  infxpenlem  8382  dcomex  8818  brdom3  8897  brdom7disj  8900  brdom6disj  8901  fpwwe2lem8  9006  fpwwe2lem9  9007  fpwwe2lem12  9010  canthwe  9020  dmrecnq  9337  xrlenlt  9643  climcau  13444  caucvgb  13453  divides  13840  vdwpc  14348  isstruct  14491  prdsleval  14723  imasaddfnlem  14774  imasvscafn  14783  invsym2  15009  funcf1  15084  funcixp  15085  funcid  15088  funcco  15089  funcsect  15090  funcinv  15091  funciso  15092  funcoppc  15093  idfucl  15099  cofuval2  15105  cofucl  15106  funcres  15114  funcres2b  15115  funcres2  15116  wunfunc  15117  funcpropd  15118  funcres2c  15119  isfull  15128  isfth  15132  fthsect  15143  fthinv  15144  fthmon  15145  fthepi  15146  ffthiso  15147  fthres2  15150  idffth  15151  cofull  15152  cofth  15153  ressffth  15156  isnat  15165  natixp  15170  nati  15173  elhomai2  15210  homa1  15213  homahom2  15214  eldmcoa  15241  coapm  15247  catcisolem  15282  catciso  15283  1stfcl  15315  2ndfcl  15316  prfcl  15321  evlfcl  15340  curf1cl  15346  curfcl  15350  hofcl  15377  yonedalem1  15390  yonedalem21  15391  yonedalem22  15396  yonffthlem  15400  yoniso  15403  pospo  15451  efgi  16528  efgi2  16534  gsum2d2lem  16787  dmdprd  16815  dprdval  16820  eldprd  16821  dprdvalOLD  16822  eldprdOLD  16823  dprd2dlem2  16874  dprd2dlem1  16875  dprd2da  16876  dprd2d2  16878  isunit  17085  subrgdvds  17221  opsrtoslem2  17915  eltopspOLD  19181  tpsexOLD  19182  lmrcl  19493  lmff  19563  2ndcctbss  19717  2ndcdisj  19718  hausdiag  19876  hauseqlcld  19877  cnextfun  20294  cnextfvval  20295  tgphaus  20345  utop2nei  20483  utop3cls  20484  ucnima  20514  xmeterval  20665  metustidOLD  20792  metustid  20793  metustsymOLD  20794  metustsym  20795  metustexhalfOLD  20796  metustexhalf  20797  elbl4  20809  metuel2  20812  isphtpc  21224  ovolfcl  21608  ovollb2lem  21629  ovolctb  21631  ovolshftlem1  21650  ovolscalem1  21654  ovolicc1  21657  ioombl1lem1  21698  ioorf  21712  dyadf  21730  eldv  22032  dvres2  22046  dvef  22111  eltayl  22484  ulmscl  22503  tglngne  23660  tgelrnln  23719  tghilbert1_1  23726  isperp  23792  brbtwn  23873  uhgraop  23969  usgracl  24016  elusuhgra  24032  usgraexmplc  24068  iswlk  24184  wlkcomp  24189  wlkcpr  24193  istrl  24203  ispth  24234  isspth  24235  2wlkeq  24371  wlknwwlknsur  24376  wlkiswwlksur  24383  isclwlk0  24418  clwlkswlks  24422  clwlkcomp  24427  wlklenvclwlk  24503  clwlkfoclwwlk  24509  isrgra  24590  isrusgra  24591  isrusgusrgcl  24597  0eusgraiff0rgracl  24605  ex-br  24817  avril1  24835  helloworld  24837  isrngo  25044  rngoablo2  25088  isdivrngo  25097  vcex  25137  h2hlm  25561  axhcompl-zf  25579  opeldifid  27117  opabdm  27125  opabrn  27126  fpwrelmap  27216  isarchi  27376  gsummpt2co  27422  prsdm  27520  prsrn  27521  qtophaus  27625  relexpindlem  28525  dfrtrclrec2  28529  rtrclreclem.trans  28532  brtpid1  28561  brtpid2  28562  brtpid3  28563  brtp  28743  dfso2  28748  dfpo2  28749  fundmpss  28761  opelco3  28773  elpredim  28821  elpredg  28823  wfrlem11  28918  frrlem5c  28958  brsymdif  29043  brv  29092  pprodss4v  29099  brsset  29104  brtxpsd  29109  sscoid  29128  dffun10  29129  brimg  29152  funpartfun  29158  funpartfv  29160  dfrdg4  29165  imagesset  29168  fvtransport  29247  brcolinear2  29273  colineardim1  29276  fvray  29356  fvline  29359  mblfinlem2  29618  areacirclem5  29677  eltail  29784  heiborlem3  29901  heiborlem4  29902  heiborlem6  29904  brabsb2  30196  eqbrrdv2  30197  fourierdlem42  31406  afveu  31662  fnopafvb  31664  tz6.12-afv  31682  tz6.12-1-afv  31683  aovprc  31697  aovrcl  31698  uhgrasiz  31799  isfusgracl  31830  fusgraimpclALT  31832  usgrafisbaseALT  31837  usgfis  31842  cmtvalN  33885  cvrval  33943
  Copyright terms: Public domain W3C validator