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

Definition df-br 4845
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 𝑅 often denotes a relation such as "< " that compares two classes 𝐴 and 𝐵, which might be numbers such as 1 and 2 (see df-ltxr 10360 for the specific definition of <). As a wff, relations are true or false. For example, (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩} → 3𝑅9) (ex-br 27615). Often class 𝑅 meets the Rel criteria to be defined in df-rel 5318, and in particular 𝑅 may be a function (see df-fun 6099). This definition of relations is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets). On the other hand, we often find uses for this definition when 𝑅 is a proper class (see for example iprc 7327). (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
df-br (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

Detailed syntax breakdown of Definition df-br
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cR . . 3 class 𝑅
41, 2, 3wbr 4844 . 2 wff 𝐴𝑅𝐵
51, 2cop 4376 . . 3 class 𝐴, 𝐵
65, 3wcel 2156 . 2 wff 𝐴, 𝐵⟩ ∈ 𝑅
74, 6wb 197 1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Colors of variables: wff setvar class
This definition is referenced by:  breq  4846  breq1  4847  breq2  4848  ssbrd  4887  nfbrd  4890  br0  4893  brne0  4894  brun  4895  brin  4896  brdif  4897  brsymdif  4903  opabss  4908  brv  5130  brabsb  5181  brabga  5184  elopabr  5208  rbropapd  5210  epelg  5225  pofun  5248  brxp  5347  opelinxp  5383  bropaex12  5394  brab2a  5396  eqbrriv  5417  eqbrrdv  5419  eqbrrdiv  5420  opeliunxp2  5462  opelco2g  5491  opelco  5495  elcnv2  5501  opelcnvg  5503  brcnvg  5504  dfdm3  5511  dfrn3  5513  elrng  5515  eldm2g  5521  breldm  5530  dmopab  5536  opelrn  5558  elrn  5567  rnopab  5571  brresg  5604  brresOLD  5608  resieq  5611  opelresi  5612  iss  5652  dfres2  5658  elidinxp  5660  elridOLD  5663  restidsing  5670  dfima3  5679  elima3  5683  imai  5688  elimasn  5700  elimasni  5702  eliniseg  5704  cotrg  5717  idrefALT  5719  idrefOLD  5720  cnvsym  5721  intasym  5722  asymref  5723  asymref2  5724  intirr  5725  codir  5727  qfto  5728  poirr2  5731  xpdifid  5773  sofld  5792  dmsnn0  5811  coiun  5859  coi1  5865  elpredim  5905  elpredg  5907  dffun4  6109  dffun5  6110  funeu2  6123  funopab  6132  funcnvsn  6146  isarep1  6184  fnop  6201  fneu2  6203  brprcneu  6396  dffv3  6400  tz6.12  6427  funopfv  6451  fnopfvb  6453  opabiota  6478  dffv2  6488  fvopab5  6527  funfvbrb  6548  dff3  6590  dff4  6591  f1ompt  6599  idref  6631  foeqcnvco  6775  f1eqcocnv  6776  fliftel  6779  fliftel1  6780  fliftcnv  6781  isof1oopb  6795  f1oiso  6821  ovprc  6907  fnotovb  6919  brabv  6925  oprabv  6929  elrnmpt2res  7000  resiexg  7328  1st2ndbr  7445  brovpreldm  7484  bropopvvv  7485  frxp  7517  xporderlem  7518  cnvimadfsn  7534  opeliunxp2f  7567  brovex  7579  ottpos  7593  dftpos3  7601  dftpos4  7602  tposoprab  7619  wfrfun  7657  wfrlem17  7663  tfrlem7  7711  tfrlem9a  7714  seqomlem2  7778  seqomlem3  7779  seqomlem4  7780  brwitnlem  7820  ercnv  7996  brdifun  8004  swoord1  8006  swoord2  8007  0er  8012  elecg  8016  iiner  8050  brecop  8071  brsdom  8211  brdom2  8218  idssen  8233  xpcomco  8285  omxpenlem  8296  brsdom2  8319  infxpenlem  9115  dcomex  9550  brdom7disj  9634  brdom6disj  9635  fpwwe2lem8  9740  fpwwe2lem9  9741  fpwwe2lem12  9744  dmrecnq  10071  xrlenlt  10384  brintclab  13961  brtrclfv  13962  dfrtrclrec2  14016  rtrclreclem3  14019  relexpindlem  14022  climcau  14620  caucvgb  14629  divides  15201  vdwpc  15897  isstruct  16077  setsstruct2  16103  prdsleval  16338  imasaddfnlem  16389  imasvscafn  16398  invsym2  16623  brcic  16658  ciclcl  16662  cicrcl  16663  cicsym  16664  funcf1  16726  funcixp  16727  funcid  16730  funcco  16731  funcsect  16732  funcinv  16733  funciso  16734  funcoppc  16735  idfucl  16741  cofuval2  16747  cofucl  16748  funcres  16756  funcres2b  16757  funcres2  16758  wunfunc  16759  funcpropd  16760  funcres2c  16761  isfull  16770  isfth  16774  fthsect  16785  fthinv  16786  fthmon  16787  fthepi  16788  ffthiso  16789  fthres2  16792  idffth  16793  cofull  16794  cofth  16795  ressffth  16798  isnat  16807  natixp  16812  nati  16815  elhomai2  16884  homa1  16887  homahom2  16888  eldmcoa  16915  coapm  16921  catcisolem  16956  catciso  16957  1stfcl  17038  2ndfcl  17039  prfcl  17044  evlfcl  17063  curf1cl  17069  curfcl  17073  hofcl  17100  yonedalem1  17113  yonedalem21  17114  yonedalem22  17119  yonffthlem  17123  yoniso  17126  pospo  17174  efgi  18329  efgi2  18335  gsum2d2lem  18569  dmdprd  18595  dprdval  18600  eldprd  18601  dprd2dlem2  18637  dprd2dlem1  18638  dprd2da  18639  dprd2d2  18641  isunit  18855  subrgdvds  18994  opsrtoslem2  19689  lmrcl  21245  lmff  21315  2ndcctbss  21468  2ndcdisj  21469  hausdiag  21658  hauseqlcld  21659  cnextfun  22077  cnextfvval  22078  cnextfres  22082  tgphaus  22129  utop2nei  22263  utop3cls  22264  ucnima  22294  xmeterval  22446  metustid  22568  metustsym  22569  metustexhalf  22570  elbl4  22577  metuel2  22579  isphtpc  23002  ovolfcl  23443  ovollb2lem  23465  ovolctb  23467  ovolshftlem1  23486  ovolscalem1  23490  ovolicc1  23493  ioombl1lem1  23535  ioorf  23550  dyadf  23568  eldv  23872  dvres2  23886  dvef  23953  eltayl  24324  ulmscl  24343  tglngne  25655  tgelrnln  25735  isperp  25817  brbtwn  25989  iswlk  26730  wlkcpr  26748  wlkcomp  26750  wlkeq  26753  wlklenvclwlk  26775  wlkreslem  26790  clwlkcomp  26899  clwlkcompbp  26902  wlkswwlksf1o  27002  wlknwwlksnsurOLD  27013  wlkwwlksurOLD  27021  clwlkclwwlkflem  27143  clwlkclwwlkfolem  27146  clwlkclwwlkfo  27148  clwlksfoclwwlkOLD  27233  wlkl0  27543  ex-br  27615  avril1  27646  helloworld  27648  vcex  27757  h2hlm  28161  axhcompl-zf  28179  opeldifid  29733  brabgaf  29741  opabdm  29744  opabrn  29745  fpwrelmap  29831  isarchi  30057  gsummpt2co  30101  qtophaus  30224  prsdm  30281  prsrn  30282  mclsax  31784  brtpid1  31919  brtpid2  31920  brtpid3  31921  brtp  31956  dfso2  31961  dfpo2  31962  fundmpss  31981  opelco3  31993  frrlem5c  32102  scutval  32227  dmscut  32234  scutf  32235  madeval2  32252  pprodss4v  32307  brsset  32312  brtxpsd  32317  sscoid  32336  dffun10  32337  brimg  32360  funpartfun  32366  funpartfv  32368  dfrecs2  32373  dfrdg4  32374  imagesset  32376  fvtransport  32455  brcolinear2  32481  colineardim1  32484  fvray  32564  fvline  32567  eltail  32685  uncf  33696  uncov  33698  unccur  33700  phpreu  33701  poimirlem26  33743  mblfinlem2  33755  areacirclem5  33811  heiborlem3  33918  heiborlem4  33919  heiborlem6  33921  isrngo  34002  rngoablo2  34014  isdivrngo  34055  brvdif2  34339  brvvdif  34340  elecALTV  34343  brresALTV  34345  inxprnres  34372  ssrel3  34379  iss2  34420  brabidga  34436  brabsb2  34636  eqbrrdv2  34637  cmtvalN  34986  cvrval  35044  undmrnresiss  38404  cnvssco  38406  cotrintab  38415  elimaint  38434  coiun1  38438  elintima  38439  briunov2  38468  brtrclfv2  38513  frege77d  38532  dfhe3  38563  dffrege76  38727  frege97  38748  frege98  38749  frege109  38760  frege110  38761  dffrege115  38766  frege131  38782  frege133  38784  rfovcnvf1od  38792  fsovrfovd  38797  fourierdlem42  40839  ovolval2lem  41333  ovolval4lem2  41340  afveu  41736  fnopafvb  41738  tz6.12-afv  41756  tz6.12-1-afv  41757  aovprc  41771  aovrcl  41772  funressndmafv2rn  41806  tz6.12-afv2  41823  tz6.12-1-afv2  41824  dfatopafv2b  41829  fnopafv2b  41832  dfafv23  41836  isupwlk  42279  sprsymrelfolem2  42305  sprsymrelf  42307  inclfusubc  42429  funcrngcsetc  42560  funcrngcsetcALT  42561  funcringcsetc  42597
  Copyright terms: Public domain W3C validator