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

Definition df-br 4367
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 9631 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 25823). Often class  R meets the  Rel criteria to be defined in df-rel 4803, and in particular  R may be a function (see df-fun 5546). 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 6686). (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 4366 . 2  wff  A R B
51, 2cop 3947 . . 3  class  <. A ,  B >.
65, 3wcel 1872 . 2  wff  <. A ,  B >.  e.  R
74, 6wb 187 1  wff  ( A R B  <->  <. A ,  B >.  e.  R )
Colors of variables: wff setvar class
This definition is referenced by:  breq  4368  breq1  4369  breq2  4370  ssbrd  4408  nfbrd  4410  br0  4413  brne0  4414  brun  4415  brin  4416  brdif  4417  brsymdif  4423  opabss  4428  brabsb  4674  brabga  4677  epelg  4708  pofun  4733  brxp  4827  brab2a  4846  bropaex12  4870  brab2ga  4872  eqbrriv  4892  eqbrrdv  4894  eqbrrdiv  4895  opeliunxp2  4935  opelco2g  4964  opelco  4968  cnvss  4969  elcnv2  4974  opelcnvg  4976  brcnvg  4977  dfdm3  4984  dfrn3  4986  elrng  4988  eldm2g  4993  breldm  5001  dmopab  5007  opelrn  5028  elrn  5037  rnopab  5041  brres  5073  brresg  5075  resieq  5077  opelresi  5078  iss  5114  dfres2  5119  restidsing  5123  dfima3  5133  elima3  5137  imai  5142  elimasn  5155  elimasni  5157  eliniseg  5159  cotrg  5173  issref  5175  cnvsym  5176  intasym  5177  asymref  5178  asymref2  5179  intirr  5180  codir  5182  qfto  5183  poirr2  5186  xpdifid  5227  sofld  5246  dmsnn0  5263  coiun  5307  coi1  5313  elpredim  5354  elpredg  5356  dffun4  5556  dffun5  5557  funeu2  5569  funopab  5577  funcnvsn  5589  isarep1  5623  fnop  5640  fneu2  5642  brprcneu  5818  dffv3  5821  tz6.12  5842  funopfv  5864  fnopfvb  5866  opabiota  5888  dffv2  5898  fvopab5  5933  funfvbrb  5954  dff3  5994  dff4  5995  f1ompt  6003  idref  6105  foeqcnvco  6157  f1eqcocnv  6158  fliftel  6161  fliftel1  6162  fliftcnv  6163  f1oiso  6201  ovprc  6279  brabv  6294  oprabv  6297  elrnmpt2res  6368  resiexg  6687  1st2ndbr  6800  bropopvvv  6831  frxp  6861  xporderlem  6862  cnvimadfsn  6878  opeliunxp2f  6911  brovex  6923  isprmpt2  6926  ottpos  6938  dftpos3  6946  dftpos4  6947  tposoprab  6964  wfrfun  7001  wfrlem17  7007  tfrlem7  7056  tfrlem9a  7059  seqomlem2  7123  seqomlem3  7124  seqomlem4  7125  brwitnlem  7164  ercnv  7339  brdifun  7345  swoord1  7347  swoord2  7348  0er  7353  elecg  7357  iiner  7390  brecop  7411  brsdom  7546  brdom2  7553  idssen  7568  xpcomco  7615  omxpenlem  7626  brsdom2  7649  infxpenlem  8396  dcomex  8828  brdom7disj  8910  brdom6disj  8911  fpwwe2lem8  9013  fpwwe2lem9  9014  fpwwe2lem12  9017  dmrecnq  9344  xrlenlt  9650  brintclab  13009  brtrclfv  13010  dfrtrclrec2  13064  rtrclreclem3  13067  relexpindlem  13070  climcau  13677  caucvgb  13689  divides  14250  vdwpc  14873  isstruct  15074  prdsleval  15318  imasaddfnlem  15377  imasvscafn  15386  invsym2  15611  brcic  15646  ciclcl  15650  cicrcl  15651  cicsym  15652  funcf1  15714  funcixp  15715  funcid  15718  funcco  15719  funcsect  15720  funcinv  15721  funciso  15722  funcoppc  15723  idfucl  15729  cofuval2  15735  cofucl  15736  funcres  15744  funcres2b  15745  funcres2  15746  wunfunc  15747  funcpropd  15748  funcres2c  15749  isfull  15758  isfth  15762  fthsect  15773  fthinv  15774  fthmon  15775  fthepi  15776  ffthiso  15777  fthres2  15780  idffth  15781  cofull  15782  cofth  15783  ressffth  15786  isnat  15795  natixp  15800  nati  15803  elhomai2  15872  homa1  15875  homahom2  15876  eldmcoa  15903  coapm  15909  catcisolem  15944  catciso  15945  1stfcl  16025  2ndfcl  16026  prfcl  16031  evlfcl  16050  curf1cl  16056  curfcl  16060  hofcl  16087  yonedalem1  16100  yonedalem21  16101  yonedalem22  16106  yonffthlem  16110  yoniso  16113  pospo  16162  efgi  17312  efgi2  17318  gsum2d2lem  17548  dmdprd  17573  dprdval  17578  eldprd  17579  dprd2dlem2  17616  dprd2dlem1  17617  dprd2da  17618  dprd2d2  17620  isunit  17828  subrgdvds  17965  opsrtoslem2  18651  lmrcl  20189  lmff  20259  2ndcctbss  20412  2ndcdisj  20413  hausdiag  20602  hauseqlcld  20603  cnextfun  21021  cnextfvval  21022  cnextfres  21026  tgphaus  21073  utop2nei  21207  utop3cls  21208  ucnima  21238  xmeterval  21389  metustid  21511  metustsym  21512  metustexhalf  21513  elbl4  21520  metuel2  21522  isphtpc  21967  ovolfcl  22361  ovollb2lem  22383  ovolctb  22385  ovolshftlem1  22404  ovolscalem1  22408  ovolicc1  22411  ioombl1lem1  22453  ioorf  22467  ioorfOLD  22472  dyadf  22491  eldv  22795  dvres2  22809  dvef  22874  eltayl  23257  ulmscl  23276  tglngne  24537  tgelrnln  24617  isperp  24699  brbtwn  24871  uhgraop  24973  usgrac  25020  elusuhgra  25037  usgraexmplc  25074  iswlk  25190  wlkcomp  25195  wlkcpr  25199  istrl  25209  ispth  25240  isspth  25241  2wlkeq  25377  wlknwwlknsur  25382  wlkiswwlksur  25389  isclwlk0  25424  clwlkswlks  25428  clwlkcomp  25433  wlklenvclwlk  25509  clwlkfoclwwlk  25515  isrgra  25596  isrusgra  25597  isrusgusrgcl  25603  0eusgraiff0rgracl  25611  ex-br  25823  avril1  25842  helloworld  25844  isrngo  26048  rngoablo2  26092  isdivrngo  26101  vcex  26141  h2hlm  26575  axhcompl-zf  26593  opeldifid  28156  brabgaf  28162  opabdm  28165  opabrn  28166  fpwrelmap  28268  isarchi  28450  gsummpt2co  28494  qtophaus  28615  prsdm  28672  prsrn  28673  mclsax  30159  brtpid1  30305  brtpid2  30306  brtpid3  30307  brtp  30340  dfso2  30345  dfpo2  30346  fundmpss  30358  opelco3  30371  frrlem5c  30471  brv  30593  pprodss4v  30600  brsset  30605  brtxpsd  30610  sscoid  30629  dffun10  30630  brimg  30653  funpartfun  30659  funpartfv  30661  dfrecs2  30666  dfrdg4  30667  imagesset  30669  fvtransport  30748  brcolinear2  30774  colineardim1  30777  fvray  30857  fvline  30860  eltail  30979  phpreu  31836  poimirlem26  31873  mblfinlem2  31885  areacirclem5  31943  heiborlem3  32052  heiborlem4  32053  heiborlem6  32055  brabsb2  32345  eqbrrdv2  32346  cmtvalN  32689  cvrval  32747  undmrnresiss  36123  cnvssco  36125  cotrintab  36134  elimaint  36153  coiun1  36157  elintima  36158  briunov2  36187  brtrclfv2  36232  frege77d  36251  dfhe3  36283  dffrege76  36448  frege97  36469  frege98  36470  frege109  36481  frege110  36482  dffrege115  36487  frege131  36503  frege133  36505  fourierdlem42  37895  fourierdlem42OLD  37896  afveu  38468  fnopafvb  38470  tz6.12-afv  38488  tz6.12-1-afv  38489  aovprc  38503  aovrcl  38504  uhgrasiz  39307  isfusgracl  39339  isfusgraclALT  39341  fusgraimpclALT2  39344  usgrafisbaseALT  39353  usgrafisbaseALT2  39354  usgfis  39359  usgfisALT  39363  inclfusubc  39468  funcrngcsetc  39601  funcrngcsetcALT  39602  funcringcsetc  39638
  Copyright terms: Public domain W3C validator