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

Definition df-br 4368
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 9544 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 25273). Often class  R meets the  Rel criteria to be defined in df-rel 4920, and in particular  R may be a function (see df-fun 5498). 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 6634). (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 4367 . 2  wff  A R B
51, 2cop 3950 . . 3  class  <. A ,  B >.
65, 3wcel 1826 . 2  wff  <. A ,  B >.  e.  R
74, 6wb 184 1  wff  ( A R B  <->  <. A ,  B >.  e.  R )
Colors of variables: wff setvar class
This definition is referenced by:  breq  4369  breq1  4370  breq2  4371  ssbrd  4408  nfbrd  4410  br0  4413  brne0  4414  brun  4415  brin  4416  brdif  4417  brsymdif  4423  opabss  4428  brabsb  4672  brabga  4675  epelg  4706  pofun  4730  brxp  4944  brab2a  4963  bropaex12  4987  brab2ga  4989  eqbrriv  5011  eqbrrdv  5013  eqbrrdiv  5014  opeliunxp2  5054  opelco2g  5083  opelco  5087  cnvss  5088  elcnv2  5093  opelcnvg  5095  brcnvg  5096  dfdm3  5103  dfrn3  5105  elrng  5107  eldm2g  5112  breldm  5120  dmopab  5126  opelrn  5147  elrn  5156  rnopab  5160  brres  5192  brresg  5194  resieq  5196  opelresi  5197  iss  5233  dfres2  5238  restidsing  5242  dfima3  5252  elima3  5256  imai  5261  elimasn  5274  elimasni  5276  eliniseg  5278  cotrg  5291  issref  5293  cnvsym  5294  intasym  5295  asymref  5296  asymref2  5297  intirr  5298  codir  5300  qfto  5301  poirr2  5304  xpdifid  5345  sofld  5364  dmsnn0  5381  coiun  5425  coi1  5431  dffun4  5508  dffun5  5509  funeu2  5521  funopab  5529  funcnvsn  5541  isarep1  5575  fnop  5592  fneu2  5594  brprcneu  5767  dffv3  5770  tz6.12  5791  funopfv  5813  fnopfvb  5815  opabiota  5837  dffv2  5847  fvopab5  5881  funfvbrb  5902  dff3  5946  dff4  5947  f1ompt  5955  idref  6054  foeqcnvco  6104  f1eqcocnv  6105  fliftel  6108  fliftel1  6109  fliftcnv  6110  f1oiso  6148  ovprc  6226  brabv  6241  oprabv  6244  elrnmpt2res  6315  resiexg  6635  1st2ndbr  6748  bropopvvv  6779  frxp  6809  xporderlem  6810  cnvimadfsn  6826  brovex  6868  isprmpt2  6871  ottpos  6883  dftpos3  6891  dftpos4  6892  tposoprab  6909  tfrlem7  6970  tfrlem9a  6973  seqomlem2  7034  seqomlem3  7035  seqomlem4  7036  brwitnlem  7075  ercnv  7250  brdifun  7256  swoord1  7258  swoord2  7259  0er  7264  elecg  7268  iiner  7301  brecop  7322  brsdom  7457  brdom2  7464  idssen  7479  xpcomco  7526  omxpenlem  7537  brsdom2  7560  infxpenlem  8304  dcomex  8740  brdom7disj  8822  brdom6disj  8823  fpwwe2lem8  8926  fpwwe2lem9  8927  fpwwe2lem12  8930  dmrecnq  9257  xrlenlt  9563  brintclab  12839  brtrclfv  12840  trclfvcotr  12847  dfrtrclrec2  12892  rtrclreclem3  12895  relexpindlem  12898  climcau  13495  caucvgb  13504  divides  13990  vdwpc  14500  isstruct  14644  prdsleval  14884  imasaddfnlem  14935  imasvscafn  14944  invsym2  15169  brcic  15204  ciclcl  15208  cicrcl  15209  cicsym  15210  funcf1  15272  funcixp  15273  funcid  15276  funcco  15277  funcsect  15278  funcinv  15279  funciso  15280  funcoppc  15281  idfucl  15287  cofuval2  15293  cofucl  15294  funcres  15302  funcres2b  15303  funcres2  15304  wunfunc  15305  funcpropd  15306  funcres2c  15307  isfull  15316  isfth  15320  fthsect  15331  fthinv  15332  fthmon  15333  fthepi  15334  ffthiso  15335  fthres2  15338  idffth  15339  cofull  15340  cofth  15341  ressffth  15344  isnat  15353  natixp  15358  nati  15361  elhomai2  15430  homa1  15433  homahom2  15434  eldmcoa  15461  coapm  15467  catcisolem  15502  catciso  15503  1stfcl  15583  2ndfcl  15584  prfcl  15589  evlfcl  15608  curf1cl  15614  curfcl  15618  hofcl  15645  yonedalem1  15658  yonedalem21  15659  yonedalem22  15664  yonffthlem  15668  yoniso  15671  pospo  15720  efgi  16854  efgi2  16860  gsum2d2lem  17115  dmdprd  17142  dprdval  17147  eldprd  17148  dprdvalOLD  17149  eldprdOLD  17150  dprd2dlem2  17202  dprd2dlem1  17203  dprd2da  17204  dprd2d2  17206  isunit  17419  subrgdvds  17556  opsrtoslem2  18262  eltopspOLD  19504  tpsexOLD  19505  lmrcl  19818  lmff  19888  2ndcctbss  20041  2ndcdisj  20042  hausdiag  20231  hauseqlcld  20232  cnextfun  20649  cnextfvval  20650  tgphaus  20700  utop2nei  20838  utop3cls  20839  ucnima  20869  xmeterval  21020  metustidOLD  21147  metustid  21148  metustsymOLD  21149  metustsym  21150  metustexhalfOLD  21151  metustexhalf  21152  elbl4  21164  metuel2  21167  isphtpc  21579  ovolfcl  21963  ovollb2lem  21984  ovolctb  21986  ovolshftlem1  22005  ovolscalem1  22009  ovolicc1  22012  ioombl1lem1  22053  ioorf  22067  dyadf  22085  eldv  22387  dvres2  22401  dvef  22466  eltayl  22840  ulmscl  22859  tglngne  24057  tgelrnln  24130  isperp  24209  brbtwn  24323  uhgraop  24425  usgrac  24472  elusuhgra  24489  usgraexmplc  24525  iswlk  24641  wlkcomp  24646  wlkcpr  24650  istrl  24660  ispth  24691  isspth  24692  2wlkeq  24828  wlknwwlknsur  24833  wlkiswwlksur  24840  isclwlk0  24875  clwlkswlks  24879  clwlkcomp  24884  wlklenvclwlk  24960  clwlkfoclwwlk  24966  isrgra  25047  isrusgra  25048  isrusgusrgcl  25054  0eusgraiff0rgracl  25062  ex-br  25273  avril1  25292  helloworld  25294  isrngo  25497  rngoablo2  25541  isdivrngo  25550  vcex  25590  h2hlm  26014  axhcompl-zf  26032  opeldifid  27589  brabgaf  27595  opabdm  27598  opabrn  27599  fpwrelmap  27706  isarchi  27879  gsummpt2co  27924  qtophaus  27993  prsdm  28050  prsrn  28051  mclsax  29118  brtpid1  29264  brtpid2  29265  brtpid3  29266  brtp  29344  dfso2  29349  dfpo2  29350  fundmpss  29362  opelco3  29373  elpredim  29421  elpredg  29423  wfrlem11  29518  frrlem5c  29558  brv  29680  pprodss4v  29687  brsset  29692  brtxpsd  29697  sscoid  29716  dffun10  29717  brimg  29740  funpartfun  29746  funpartfv  29748  dfrdg4  29753  imagesset  29756  fvtransport  29835  brcolinear2  29861  colineardim1  29864  fvray  29944  fvline  29947  mblfinlem2  30217  areacirclem5  30277  eltail  30358  heiborlem3  30475  heiborlem4  30476  heiborlem6  30478  brabsb2  30769  eqbrrdv2  30770  fourierdlem42  32097  afveu  32404  fnopafvb  32406  tz6.12-afv  32424  tz6.12-1-afv  32425  aovprc  32439  aovrcl  32440  uhgrasiz  32712  isfusgracl  32744  isfusgraclALT  32746  fusgraimpclALT2  32749  usgrafisbaseALT  32758  usgrafisbaseALT2  32759  usgfis  32764  usgfisALT  32768  inclfusubc  32873  funcrngcsetc  33006  funcrngcsetcALT  33007  funcringcsetc  33043  cmtvalN  35349  cvrval  35407  coiun1  38189  elimaint  38194  elintima  38195  briunov2  38220  brtrclfv2  38258  dfhe3  38269  dffrege76  38438  frege97  38459  frege98  38460  frege109  38471  frege110  38472  dffrege115  38477  frege131  38493  frege133  38495
  Copyright terms: Public domain W3C validator