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

Definition df-br 4205
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 9114 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 21727). Often class  R meets the  Rel criteria to be defined in df-rel 4876, and in particular  R may be a function (see df-fun 5447). 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 4204 . 2  wff  A R B
51, 2cop 3809 . . 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  4206  breq1  4207  breq2  4208  ssbrd  4245  nfbrd  4247  brun  4250  brin  4251  brdif  4252  opabss  4261  brabsbOLD  4456  brabsb  4458  brabga  4461  epelg  4487  pofun  4511  brxp  4900  brab2a  4918  brab2ga  4942  eqbrriv  4962  eqbrrdv  4964  eqbrrdiv  4965  opeliunxp2  5004  opelco2g  5031  opelco  5035  cnvss  5036  elcnv2  5041  opelcnvg  5043  brcnvg  5044  dfdm3  5049  dfrn3  5051  elrng  5053  eldm2g  5057  breldm  5065  dmopab  5071  opelrn  5092  elrn  5101  rnopab  5106  brres  5143  brresg  5145  resieq  5147  opelresiOLD  5148  opelresi  5149  resiexg  5179  iss  5180  dfres2  5184  dfima3  5197  elima3  5201  imai  5209  elimasn  5220  elimasni  5222  eliniseg  5224  cotr  5237  issref  5238  cnvsym  5239  intasym  5240  asymref  5241  asymref2  5242  intirr  5243  codir  5245  qfto  5246  poirr2  5249  sofld  5309  dmsnn0  5326  coiun  5370  co02  5374  coi1  5376  dffun4  5457  dffun5  5458  funeu2  5469  funopab  5477  funcnvsn  5487  isarep1  5523  fnop  5539  fneu2  5541  brprcneu  5712  dffv3  5715  tz6.12  5739  funopfv  5757  fnopfvb  5759  dffv2  5787  funfvbrb  5834  dff3  5873  dff4  5874  f1ompt  5882  idref  5970  foeqcnvco  6018  f1eqcocnv  6019  fliftel  6022  fliftel1  6023  fliftcnv  6024  f1oiso  6062  ovprc  6099  brabv  6111  1st2ndbr  6387  bropopvvv  6417  frxp  6447  xporderlem  6448  brovex  6465  isprmpt2  6468  ottpos  6480  dftpos3  6488  dftpos4  6489  tposoprab  6506  fvopab5  6525  opabiota  6529  tfrlem9a  6638  seqomlem2  6699  seqomlem3  6700  seqomlem4  6701  0we1  6741  brwitnlem  6742  ercnv  6917  brdifun  6923  swoord1  6925  swoord2  6926  0er  6931  elecg  6934  iiner  6967  brecop  6988  brsdom  7121  brdom2  7128  idssen  7143  xpcomco  7189  omxpenlem  7200  brsdom2  7222  infxpenlem  7884  dcomex  8316  brdom3  8395  brdom7disj  8398  brdom6disj  8399  fpwwe2lem8  8501  fpwwe2lem9  8502  fpwwe2lem12  8505  canthwe  8515  dmrecnq  8834  xrlenlt  9132  climcau  12452  caucvgb  12461  divides  12842  vdwpc  13336  isstruct  13467  prdsleval  13687  imasaddfnlem  13741  imasvscafn  13750  invsym2  13976  funcf1  14051  funcixp  14052  funcid  14055  funcco  14056  funcsect  14057  funcinv  14058  funciso  14059  funcoppc  14060  idfucl  14066  cofuval2  14072  cofucl  14073  funcres  14081  funcres2b  14082  funcres2  14083  wunfunc  14084  funcpropd  14085  funcres2c  14086  isfull  14095  isfth  14099  fthsect  14110  fthinv  14111  fthmon  14112  fthepi  14113  ffthiso  14114  fthres2  14117  idffth  14118  cofull  14119  cofth  14120  ressffth  14123  isnat  14132  natixp  14137  nati  14140  elhomai2  14177  homa1  14180  homahom2  14181  eldmcoa  14208  coapm  14214  catcisolem  14249  catciso  14250  1stfcl  14282  2ndfcl  14283  prfcl  14288  evlfcl  14307  curf1cl  14313  curfcl  14317  hofcl  14344  yonedalem1  14357  yonedalem21  14358  yonedalem22  14363  yonffthlem  14367  yoniso  14370  pospo  14418  efgi  15339  efgi2  15345  gsum2d2lem  15535  dmdprd  15547  dprdval  15549  eldprd  15550  dprd2dlem2  15586  dprd2dlem1  15587  dprd2da  15588  dprd2d2  15590  isunit  15750  subrgdvds  15870  opsrtoslem2  16533  eltopspOLD  16971  tpsexOLD  16972  lmrcl  17283  lmff  17353  2ndcctbss  17506  2ndcdisj  17507  hausdiag  17665  hauseqlcld  17666  cnextfun  18083  cnextfvval  18084  tgphaus  18134  utop2nei  18268  utop3cls  18269  ucnima  18299  xmeterval  18450  metustidOLD  18577  metustid  18578  metustsymOLD  18579  metustsym  18580  metustexhalfOLD  18581  metustexhalf  18582  elbl4  18594  metuel2  18597  isphtpc  19007  ovolfcl  19351  ovollb2lem  19372  ovolctb  19374  ovolshftlem1  19393  ovolscalem1  19397  ovolicc1  19400  ioombl1lem1  19440  ioorf  19453  dyadf  19471  eldv  19773  dvres2  19787  dvef  19852  eltayl  20264  ulmscl  20283  iswlk  21515  istrl  21525  ispth  21556  isspth  21557  ex-br  21727  avril1  21745  helloworld  21747  isrngo  21954  rngoablo2  21998  isdivrngo  22007  vcex  22047  h2hlm  22471  axhcompl-zf  22489  isarchi  24240  relexpindlem  25127  dfrtrclrec2  25131  rtrclreclem.trans  25134  brtpid1  25166  brtpid2  25167  brtpid3  25168  brtp  25361  dfso2  25366  dfpo2  25367  fundmpss  25377  elpredim  25431  elpredg  25433  wfrlem11  25521  frrlem5c  25542  brsymdif  25627  brv  25672  pprodss4v  25679  brsset  25684  brtxpsd  25689  sscoid  25708  dffun10  25709  brimg  25732  funpartfun  25738  funpartfv  25740  dfrdg4  25745  imagesset  25748  brbtwn  25786  fvtransport  25914  brcolinear2  25940  colineardim1  25943  fvray  26023  fvline  26026  mblfinlem  26190  areacirclem6  26233  eltail  26340  heiborlem3  26459  heiborlem4  26460  heiborlem6  26462  brabsb2  26648  eqbrrdv2  26649  afveu  27931  fnopafvb  27933  tz6.12-afv  27951  tz6.12-1-afv  27952  aovprc  27966  aovrcl  27967  cmtvalN  29848  cvrval  29906
  Copyright terms: Public domain W3C validator