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  23881  relexpindlem  24036  dfrtrclrec2  24040  rtrclreclem.trans  24043  brtpid1  24075  brtpid2  24076  brtpid3  24077  brtp  24106  dfso2  24111  dfpo2  24112  fundmpss  24122  elpredim  24176  elpredg  24178  wfrlem11  24266  frrlem5c  24287  brsymdif  24372  brv  24417  pprodss4v  24424  brsset  24429  brtxpsd  24434  dffun10  24453  brimg  24476  funpartfun  24481  funpartfv  24483  dfrdg4  24488  brbtwn  24527  fvtransport  24655  brcolinear2  24681  colineardim1  24684  fvray  24764  fvline  24767  areacirclem6  24930  restidsing  25076  prj1b  25079  prj3  25080  domintrefc  25125  deref  25288  dfdir2  25291  vecval1b  25451  glmrngo  25482  bosser  26167  eltail  26323  heiborlem3  26537  heiborlem4  26538  heiborlem6  26540  brabsb2  26730  eqbrrdv2  26731  fnopafvb  28017  aovprc  28048  aovrcl  28049  cmtvalN  29401  cvrval  29459
  Copyright terms: Public domain W3C validator