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

Definition df-br 3984
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 8826 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 20747). Often class  R meets the  Rel criteria to be defined in df-rel 4662, and in particular  R may be a function (see df-fun 4669). 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 3983 . 2  wff  A R B
51, 2cop 3603 . . 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  3985  breq1  3986  breq2  3987  ssbrd  4024  nfbrd  4026  brun  4029  brin  4030  brdif  4031  opabss  4040  brabsbOLD  4232  brabsb  4234  brabga  4237  epelg  4264  pofun  4288  brxp  4694  brab2a  4712  brab2ga  4737  eqbrriv  4756  eqbrrdv  4758  eqbrrdiv  4759  opeliunxp2  4798  opelco2g  4825  opelco  4827  cnvss  4828  elcnv2  4833  opelcnvg  4835  brcnvg  4836  dfdm3  4841  dfrn3  4843  elrng  4845  eldm2g  4849  breldm  4857  dmopab  4863  opelrn  4884  elrn  4893  rnopab  4898  brres  4935  brresg  4937  resieq  4939  opelresiOLD  4940  opelresi  4941  resiexg  4971  iss  4972  dfres2  4976  dfima3  4989  elima3  4993  imai  5001  elimasn  5012  elimasni  5014  eliniseg  5016  cotr  5029  issref  5030  cnvsym  5031  intasym  5032  asymref  5033  asymref2  5034  intirr  5035  codir  5037  qfto  5038  poirr2  5041  sofld  5095  dmsnn0  5111  coiun  5155  co02  5159  coi1  5161  dffun4  5192  dffun5  5193  funeu2  5204  funopab  5212  funcnvsn  5221  isarep1  5255  fnop  5271  fneu2  5273  fv2  5440  tz6.12  5464  funopfv  5482  fnopfvb  5484  dffv2  5512  funfvbrb  5558  dff3  5593  dff4  5594  f1ompt  5602  idref  5679  foeqcnvco  5724  f1eqcocnv  5725  fliftel  5728  fliftel1  5729  fliftcnv  5730  f1oiso  5768  ovprc  5805  1st2ndbr  6089  frxp  6145  xporderlem  6146  ottpos  6164  dftpos3  6172  dftpos4  6173  tposoprab  6190  fvopab5  6241  opabiota  6245  tfrlem9a  6356  seqomlem2  6417  seqomlem3  6418  seqomlem4  6419  0we1  6459  brwitnlem  6460  ercnv  6635  brdifun  6641  swoord1  6643  swoord2  6644  0er  6649  elecg  6652  iiner  6685  brecop  6705  brsdom  6838  brdom2  6845  idssen  6860  xpcomco  6906  omxpenlem  6917  brsdom2  6939  infxpenlem  7595  dcomex  8027  brdom3  8107  brdom7disj  8110  brdom6disj  8111  fpwwe2lem8  8213  fpwwe2lem9  8214  fpwwe2lem12  8217  canthwe  8227  dmrecnq  8546  xrlenlt  8844  climcau  12095  caucvgb  12103  divides  12481  vdwpc  12975  isstruct  13106  prdsleval  13324  imasaddfnlem  13378  imasvscafn  13387  invsym2  13613  funcf1  13688  funcixp  13689  funcid  13692  funcco  13693  funcsect  13694  funcinv  13695  funciso  13696  funcoppc  13697  idfucl  13703  cofuval2  13709  cofucl  13710  funcres  13718  funcres2b  13719  funcres2  13720  wunfunc  13721  funcpropd  13722  funcres2c  13723  isfull  13732  isfth  13736  fthsect  13747  fthinv  13748  fthmon  13749  fthepi  13750  ffthiso  13751  fthres2  13754  idffth  13755  cofull  13756  cofth  13757  ressffth  13760  isnat  13769  natixp  13774  nati  13777  elhomai2  13814  homa1  13817  homahom2  13818  eldmcoa  13845  coapm  13851  catcisolem  13886  catciso  13887  1stfcl  13919  2ndfcl  13920  prfcl  13925  evlfcl  13944  curf1cl  13950  curfcl  13954  hofcl  13981  yonedalem1  13994  yonedalem21  13995  yonedalem22  14000  yonffthlem  14004  yoniso  14007  pospo  14055  efgi  14976  efgi2  14982  gsum2d2lem  15172  dmdprd  15184  dprdval  15186  eldprd  15187  dprd2dlem2  15223  dprd2dlem1  15224  dprd2da  15225  dprd2d2  15227  isunit  15387  subrgdvds  15507  opsrtoslem2  16174  eltopspOLD  16604  tpsexOLD  16605  lmrcl  16909  lmff  16977  2ndcctbss  17129  2ndcdisj  17130  hausdiag  17287  hauseqlcld  17288  tgphaus  17747  xmeterval  17926  isphtpc  18440  ovolfcl  18774  ovollb2lem  18795  ovolctb  18797  ovolshftlem1  18816  ovolscalem1  18820  ovolicc1  18823  ioombl1lem1  18863  ioorf  18876  dyadf  18894  eldv  19196  dvres2  19210  dvef  19275  eltayl  19687  ulmscl  19706  ex-br  20747  avril1  20782  helloworld  20784  isrngo  20991  rngoablo2  21035  isdivrngo  21044  vcex  21082  h2hlm  21506  axhcompl-zf  21524  iseupa  23239  relexpindlem  23394  dfrtrclrec2  23398  rtrclreclem.trans  23401  brtpid1  23433  brtpid2  23434  brtpid3  23435  brtp  23463  dfso2  23468  dfpo2  23469  fundmpss  23477  elpredim  23531  elpredg  23533  wfrlem11  23621  frrlem5c  23642  brsymdif  23734  brv  23779  pprodss4v  23786  brsset  23791  brtxpsd  23796  brimg  23837  funpartfun  23842  funpartfv  23844  dfrdg4  23849  brbtwn  23888  fvtransport  24016  brcolinear2  24042  colineardim1  24045  fvray  24125  fvline  24128  restidsing  24428  prj1b  24431  prj3  24432  domintrefc  24478  deref  24641  dfdir2  24644  vecval1b  24804  glmrngo  24835  bosser  25520  eltail  25676  heiborlem3  25890  heiborlem4  25891  heiborlem6  25893  brabsb2  26083  eqbrrdv2  26084  cmtvalN  28552  cvrval  28610
  Copyright terms: Public domain W3C validator