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

Definition df-br 4427
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 9679 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 25726). Often class  R meets the  Rel criteria to be defined in df-rel 4861, and in particular  R may be a function (see df-fun 5603). 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 6742). (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 4426 . 2  wff  A R B
51, 2cop 4008 . . 3  class  <. A ,  B >.
65, 3wcel 1870 . 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  4428  breq1  4429  breq2  4430  ssbrd  4467  nfbrd  4469  br0  4472  brne0  4473  brun  4474  brin  4475  brdif  4476  brsymdif  4482  opabss  4487  brabsb  4732  brabga  4735  epelg  4766  pofun  4791  brxp  4885  brab2a  4904  bropaex12  4928  brab2ga  4930  eqbrriv  4950  eqbrrdv  4952  eqbrrdiv  4953  opeliunxp2  4993  opelco2g  5022  opelco  5026  cnvss  5027  elcnv2  5032  opelcnvg  5034  brcnvg  5035  dfdm3  5042  dfrn3  5044  elrng  5046  eldm2g  5051  breldm  5059  dmopab  5065  opelrn  5086  elrn  5095  rnopab  5099  brres  5131  brresg  5133  resieq  5135  opelresi  5136  iss  5172  dfres2  5177  restidsing  5181  dfima3  5191  elima3  5195  imai  5200  elimasn  5213  elimasni  5215  eliniseg  5217  cotrg  5231  issref  5233  cnvsym  5234  intasym  5235  asymref  5236  asymref2  5237  intirr  5238  codir  5240  qfto  5241  poirr2  5244  xpdifid  5285  sofld  5304  dmsnn0  5321  coiun  5365  coi1  5371  elpredim  5411  elpredg  5413  dffun4  5613  dffun5  5614  funeu2  5626  funopab  5634  funcnvsn  5646  isarep1  5680  fnop  5697  fneu2  5699  brprcneu  5874  dffv3  5877  tz6.12  5898  funopfv  5920  fnopfvb  5922  opabiota  5944  dffv2  5954  fvopab5  5989  funfvbrb  6010  dff3  6050  dff4  6051  f1ompt  6059  idref  6161  foeqcnvco  6213  f1eqcocnv  6214  fliftel  6217  fliftel1  6218  fliftcnv  6219  f1oiso  6257  ovprc  6335  brabv  6350  oprabv  6353  elrnmpt2res  6424  resiexg  6743  1st2ndbr  6856  bropopvvv  6887  frxp  6917  xporderlem  6918  cnvimadfsn  6934  brovex  6976  isprmpt2  6979  ottpos  6991  dftpos3  6999  dftpos4  7000  tposoprab  7017  wfrfun  7054  wfrlem17  7060  tfrlem7  7109  tfrlem9a  7112  seqomlem2  7176  seqomlem3  7177  seqomlem4  7178  brwitnlem  7217  ercnv  7392  brdifun  7398  swoord1  7400  swoord2  7401  0er  7406  elecg  7410  iiner  7443  brecop  7464  brsdom  7599  brdom2  7606  idssen  7621  xpcomco  7668  omxpenlem  7679  brsdom2  7702  infxpenlem  8443  dcomex  8875  brdom7disj  8957  brdom6disj  8958  fpwwe2lem8  9061  fpwwe2lem9  9062  fpwwe2lem12  9065  dmrecnq  9392  xrlenlt  9698  brintclab  13044  brtrclfv  13045  dfrtrclrec2  13099  rtrclreclem3  13102  relexpindlem  13105  climcau  13712  caucvgb  13724  divides  14285  vdwpc  14893  isstruct  15094  prdsleval  15334  imasaddfnlem  15385  imasvscafn  15394  invsym2  15619  brcic  15654  ciclcl  15658  cicrcl  15659  cicsym  15660  funcf1  15722  funcixp  15723  funcid  15726  funcco  15727  funcsect  15728  funcinv  15729  funciso  15730  funcoppc  15731  idfucl  15737  cofuval2  15743  cofucl  15744  funcres  15752  funcres2b  15753  funcres2  15754  wunfunc  15755  funcpropd  15756  funcres2c  15757  isfull  15766  isfth  15770  fthsect  15781  fthinv  15782  fthmon  15783  fthepi  15784  ffthiso  15785  fthres2  15788  idffth  15789  cofull  15790  cofth  15791  ressffth  15794  isnat  15803  natixp  15808  nati  15811  elhomai2  15880  homa1  15883  homahom2  15884  eldmcoa  15911  coapm  15917  catcisolem  15952  catciso  15953  1stfcl  16033  2ndfcl  16034  prfcl  16039  evlfcl  16058  curf1cl  16064  curfcl  16068  hofcl  16095  yonedalem1  16108  yonedalem21  16109  yonedalem22  16114  yonffthlem  16118  yoniso  16121  pospo  16170  efgi  17304  efgi2  17310  gsum2d2lem  17540  dmdprd  17565  dprdval  17570  eldprd  17571  dprd2dlem2  17608  dprd2dlem1  17609  dprd2da  17610  dprd2d2  17612  isunit  17820  subrgdvds  17957  opsrtoslem2  18643  lmrcl  20178  lmff  20248  2ndcctbss  20401  2ndcdisj  20402  hausdiag  20591  hauseqlcld  20592  cnextfun  21010  cnextfvval  21011  cnextfres  21015  tgphaus  21062  utop2nei  21196  utop3cls  21197  ucnima  21227  xmeterval  21378  metustid  21500  metustsym  21501  metustexhalf  21502  elbl4  21509  metuel2  21511  isphtpc  21918  ovolfcl  22298  ovollb2lem  22319  ovolctb  22321  ovolshftlem1  22340  ovolscalem1  22344  ovolicc1  22347  ioombl1lem1  22388  ioorf  22402  ioorfOLD  22407  dyadf  22426  eldv  22730  dvres2  22744  dvef  22809  eltayl  23180  ulmscl  23199  tglngne  24455  tgelrnln  24534  isperp  24614  brbtwn  24775  uhgraop  24877  usgrac  24924  elusuhgra  24941  usgraexmplc  24977  iswlk  25093  wlkcomp  25098  wlkcpr  25102  istrl  25112  ispth  25143  isspth  25144  2wlkeq  25280  wlknwwlknsur  25285  wlkiswwlksur  25292  isclwlk0  25327  clwlkswlks  25331  clwlkcomp  25336  wlklenvclwlk  25412  clwlkfoclwwlk  25418  isrgra  25499  isrusgra  25500  isrusgusrgcl  25506  0eusgraiff0rgracl  25514  ex-br  25726  avril1  25745  helloworld  25747  isrngo  25951  rngoablo2  25995  isdivrngo  26004  vcex  26044  h2hlm  26468  axhcompl-zf  26486  opeldifid  28049  brabgaf  28055  opabdm  28058  opabrn  28059  fpwrelmap  28161  isarchi  28337  gsummpt2co  28381  qtophaus  28502  prsdm  28559  prsrn  28560  mclsax  29995  brtpid1  30141  brtpid2  30142  brtpid3  30143  brtp  30176  dfso2  30181  dfpo2  30182  fundmpss  30194  opelco3  30207  frrlem5c  30307  brv  30429  pprodss4v  30436  brsset  30441  brtxpsd  30446  sscoid  30465  dffun10  30466  brimg  30489  funpartfun  30495  funpartfv  30497  dfrecs2  30502  dfrdg4  30503  imagesset  30505  fvtransport  30584  brcolinear2  30610  colineardim1  30613  fvray  30693  fvline  30696  eltail  30815  phpreu  31633  poimirlem26  31670  mblfinlem2  31682  areacirclem5  31740  heiborlem3  31849  heiborlem4  31850  heiborlem6  31852  brabsb2  32142  eqbrrdv2  32143  cmtvalN  32486  cvrval  32544  elimaint  35879  coiun1  35883  elintima  35884  briunov2  35913  brtrclfv2  35958  frege77d  35977  dfhe3  36007  dffrege76  36172  frege97  36193  frege98  36194  frege109  36205  frege110  36206  dffrege115  36211  frege131  36227  frege133  36229  fourierdlem42  37580  afveu  38045  fnopafvb  38047  tz6.12-afv  38065  tz6.12-1-afv  38066  aovprc  38080  aovrcl  38081  uhgrasiz  38464  isfusgracl  38496  isfusgraclALT  38498  fusgraimpclALT2  38501  usgrafisbaseALT  38510  usgrafisbaseALT2  38511  usgfis  38516  usgfisALT  38520  inclfusubc  38625  funcrngcsetc  38758  funcrngcsetcALT  38759  funcringcsetc  38795
  Copyright terms: Public domain W3C validator