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

Definition df-br 4024
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 8872 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 20818). Often class  R meets the  Rel criteria to be defined in df-rel 4696, and in particular  R may be a function (see df-fun 5257). 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 4023 . 2  wff  A R B
51, 2cop 3643 . . 3  class  <. A ,  B >.
65, 3wcel 1684 . 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  4025  breq1  4026  breq2  4027  ssbrd  4064  nfbrd  4066  brun  4069  brin  4070  brdif  4071  opabss  4080  brabsbOLD  4274  brabsb  4276  brabga  4279  epelg  4306  pofun  4330  brxp  4720  brab2a  4738  brab2ga  4763  eqbrriv  4782  eqbrrdv  4784  eqbrrdiv  4785  opeliunxp2  4824  opelco2g  4851  opelco  4853  cnvss  4854  elcnv2  4859  opelcnvg  4861  brcnvg  4862  dfdm3  4867  dfrn3  4869  elrng  4871  eldm2g  4875  breldm  4883  dmopab  4889  opelrn  4910  elrn  4919  rnopab  4924  brres  4961  brresg  4963  resieq  4965  opelresiOLD  4966  opelresi  4967  resiexg  4997  iss  4998  dfres2  5002  dfima3  5015  elima3  5019  imai  5027  elimasn  5038  elimasni  5040  eliniseg  5042  cotr  5055  issref  5056  cnvsym  5057  intasym  5058  asymref  5059  asymref2  5060  intirr  5061  codir  5063  qfto  5064  poirr2  5067  sofld  5121  dmsnn0  5138  coiun  5182  co02  5186  coi1  5188  dffun4  5267  dffun5  5268  funeu2  5279  funopab  5287  funcnvsn  5297  isarep1  5331  fnop  5347  fneu2  5349  brprcneu  5518  dffv3  5521  tz6.12  5545  funopfv  5562  fnopfvb  5564  dffv2  5592  funfvbrb  5638  dff3  5673  dff4  5674  f1ompt  5682  idref  5759  foeqcnvco  5804  f1eqcocnv  5805  fliftel  5808  fliftel1  5809  fliftcnv  5810  f1oiso  5848  ovprc  5885  1st2ndbr  6169  frxp  6225  xporderlem  6226  ottpos  6244  dftpos3  6252  dftpos4  6253  tposoprab  6270  fvopab5  6289  opabiota  6293  tfrlem9a  6402  seqomlem2  6463  seqomlem3  6464  seqomlem4  6465  0we1  6505  brwitnlem  6506  ercnv  6681  brdifun  6687  swoord1  6689  swoord2  6690  0er  6695  elecg  6698  iiner  6731  brecop  6751  brsdom  6884  brdom2  6891  idssen  6906  xpcomco  6952  omxpenlem  6963  brsdom2  6985  infxpenlem  7641  dcomex  8073  brdom3  8153  brdom7disj  8156  brdom6disj  8157  fpwwe2lem8  8259  fpwwe2lem9  8260  fpwwe2lem12  8263  canthwe  8273  dmrecnq  8592  xrlenlt  8890  climcau  12144  caucvgb  12152  divides  12533  vdwpc  13027  isstruct  13158  prdsleval  13376  imasaddfnlem  13430  imasvscafn  13439  invsym2  13665  funcf1  13740  funcixp  13741  funcid  13744  funcco  13745  funcsect  13746  funcinv  13747  funciso  13748  funcoppc  13749  idfucl  13755  cofuval2  13761  cofucl  13762  funcres  13770  funcres2b  13771  funcres2  13772  wunfunc  13773  funcpropd  13774  funcres2c  13775  isfull  13784  isfth  13788  fthsect  13799  fthinv  13800  fthmon  13801  fthepi  13802  ffthiso  13803  fthres2  13806  idffth  13807  cofull  13808  cofth  13809  ressffth  13812  isnat  13821  natixp  13826  nati  13829  elhomai2  13866  homa1  13869  homahom2  13870  eldmcoa  13897  coapm  13903  catcisolem  13938  catciso  13939  1stfcl  13971  2ndfcl  13972  prfcl  13977  evlfcl  13996  curf1cl  14002  curfcl  14006  hofcl  14033  yonedalem1  14046  yonedalem21  14047  yonedalem22  14052  yonffthlem  14056  yoniso  14059  pospo  14107  efgi  15028  efgi2  15034  gsum2d2lem  15224  dmdprd  15236  dprdval  15238  eldprd  15239  dprd2dlem2  15275  dprd2dlem1  15276  dprd2da  15277  dprd2d2  15279  isunit  15439  subrgdvds  15559  opsrtoslem2  16226  eltopspOLD  16656  tpsexOLD  16657  lmrcl  16961  lmff  17029  2ndcctbss  17181  2ndcdisj  17182  hausdiag  17339  hauseqlcld  17340  tgphaus  17799  xmeterval  17978  isphtpc  18492  ovolfcl  18826  ovollb2lem  18847  ovolctb  18849  ovolshftlem1  18868  ovolscalem1  18872  ovolicc1  18875  ioombl1lem1  18915  ioorf  18928  dyadf  18946  eldv  19248  dvres2  19262  dvef  19327  eltayl  19739  ulmscl  19758  ex-br  20818  avril1  20836  helloworld  20838  isrngo  21045  rngoablo2  21089  isdivrngo  21098  vcex  21136  h2hlm  21560  axhcompl-zf  21578  iseupa  23292  relexpindlem  23447  dfrtrclrec2  23451  rtrclreclem.trans  23454  brtpid1  23486  brtpid2  23487  brtpid3  23488  brtp  23517  dfso2  23522  dfpo2  23523  fundmpss  23533  elpredim  23587  elpredg  23589  wfrlem11  23677  frrlem5c  23698  brsymdif  23783  brv  23828  pprodss4v  23835  brsset  23840  brtxpsd  23845  dffun10  23864  brimg  23887  funpartfun  23892  funpartfv  23894  dfrdg4  23899  brbtwn  23938  fvtransport  24066  brcolinear2  24092  colineardim1  24095  fvray  24175  fvline  24178  areacirclem6  24342  restidsing  24488  prj1b  24491  prj3  24492  domintrefc  24537  deref  24700  dfdir2  24703  vecval1b  24863  glmrngo  24894  bosser  25579  eltail  25735  heiborlem3  25949  heiborlem4  25950  heiborlem6  25952  brabsb2  26142  eqbrrdv2  26143  fnopafvb  27429  aovprc  27460  aovrcl  27461  cmtvalN  28774  cvrval  28832
  Copyright terms: Public domain W3C validator