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 5079
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 10998 for the specific definition of <). As a wff, relations are true or false. For example, (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩} → 3𝑅9) (ex-br 28774). Often class 𝑅 meets the Rel criteria to be defined in df-rel 5595, and in particular 𝑅 may be a function (see df-fun 6432). 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 7747). (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 5078 . 2 wff 𝐴𝑅𝐵
51, 2cop 4572 . . 3 class 𝐴, 𝐵
65, 3wcel 2109 . 2 wff 𝐴, 𝐵⟩ ∈ 𝑅
74, 6wb 205 1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Colors of variables: wff setvar class
This definition is referenced by:  breq  5080  breq1  5081  breq2  5082  ssbrd  5121  nfbrd  5124  br0  5127  brne0  5128  brun  5129  brin  5130  brdif  5131  brsymdif  5137  opabss  5142  brv  5389  brsnop  5438  brabsb  5445  brabga  5448  elopabr  5474  rbropapd  5476  brabv  5481  epelg  5495  pofun  5520  brxp  5635  opelinxp  5665  bropaex12  5676  brab2a  5678  eqbrriv  5698  eqbrrdv  5700  eqbrrdiv  5701  opeliunxp2  5744  opelco2g  5773  opelco  5777  elcnv2  5783  opelcnvg  5786  dfdm3  5793  dfrn3  5795  elrng  5797  eldm2g  5805  breldm  5814  dmopab  5821  opelrn  5849  rnopab  5860  brres  5895  resieq  5899  opelidres  5900  iss  5940  dfres2  5946  elidinxp  5948  restidsing  5959  dfima3  5969  elima3  5973  imai  5979  elimasng  5993  cotrg  6013  idrefALT  6015  cnvsym  6016  intasym  6017  asymref  6018  asymref2  6019  intirr  6020  codir  6022  qfto  6023  poirr2  6026  xpdifid  6068  sofld  6087  dmsnn0  6107  coiun  6157  coi1  6163  dfpo2  6196  dffun4  6442  dffun5  6443  funeu2  6456  funopab  6465  funcnvsn  6480  isarep1  6518  fnop  6538  fneu2  6540  brprcneu  6759  fvprc  6760  dffv3  6764  tz6.12  6791  funopfv  6815  fnopfvb  6817  opabiota  6845  dffv2  6857  fvopab5  6901  funfvbrb  6922  dff3  6970  dff4  6971  f1ompt  6979  idref  7012  foeqcnvco  7165  f1eqcocnv  7166  f1eqcocnvOLD  7167  fliftel  7173  fliftel1  7174  fliftcnv  7175  isof1oopb  7189  f1oiso  7215  ovprc  7306  fnotovb  7318  oprabv  7326  elrnmpores  7402  1st2ndbr  7869  brovpreldm  7913  bropopvvv  7914  frxp  7951  xporderlem  7952  cnvimadfsn  7972  opeliunxp2f  8010  brovex  8022  ottpos  8036  dftpos3  8044  dftpos4  8045  tposoprab  8062  frrlem9  8094  fprresex  8110  wfrfunOLD  8134  wfrlem17OLD  8140  tfrlem7  8198  tfrlem9a  8201  seqomlem2  8266  seqomlem3  8267  seqomlem4  8268  brwitnlem  8313  ercnv  8493  brdifun  8501  swoord1  8503  swoord2  8504  0er  8509  elecg  8515  iiner  8552  brecop  8573  brsdom  8734  brdom2  8741  idssen  8756  xpcomco  8818  omxpenlem  8829  brsdom2  8853  ssttrcl  9434  ttrcltr  9435  ttrclss  9439  infxpenlem  9753  dcomex  10187  brdom7disj  10271  brdom6disj  10272  fpwwe2lem7  10377  fpwwe2lem8  10378  fpwwe2lem11  10381  dmrecnq  10708  xrlenlt  11024  brintclab  14693  brtrclfv  14694  dfrtrclrec2  14750  rtrclreclem3  14752  relexpindlem  14755  climcau  15363  caucvgb  15372  divides  15946  vdwpc  16662  isstruct  16834  setsstruct2  16856  prdsleval  17169  imasaddfnlem  17220  imasvscafn  17229  invsym2  17456  brcic  17491  ciclcl  17495  cicrcl  17496  cicsym  17497  funcf1  17562  funcixp  17563  funcid  17566  funcco  17567  funcsect  17568  funcinv  17569  funciso  17570  funcoppc  17571  idfucl  17577  cofuval2  17583  cofucl  17584  funcres  17592  funcres2b  17593  funcres2  17594  wunfunc  17595  wunfuncOLD  17596  funcpropd  17597  funcres2c  17598  isfull  17607  isfth  17611  fthsect  17622  fthinv  17623  fthmon  17624  fthepi  17625  ffthiso  17626  fthres2  17629  idffth  17630  cofull  17631  cofth  17632  ressffth  17635  isnat  17644  natixp  17649  nati  17652  elhomai2  17730  homa1  17733  homahom2  17734  eldmcoa  17761  coapm  17767  catcisolem  17806  catciso  17807  1stfcl  17895  2ndfcl  17896  prfcl  17901  evlfcl  17921  curf1cl  17927  curfcl  17931  hofcl  17958  yonedalem1  17971  yonedalem21  17972  yonedalem22  17977  yonffthlem  17981  yoniso  17984  pospo  18044  efgi  19306  efgi2  19312  gsum2d2lem  19555  gsumxp2  19562  dmdprd  19582  dprdval  19587  eldprd  19588  dprd2dlem2  19624  dprd2dlem1  19625  dprd2da  19626  dprd2d2  19628  isunit  19880  subrgdvds  20019  opsrtoslem2  21244  lmrcl  22363  lmff  22433  2ndcctbss  22587  2ndcdisj  22588  hausdiag  22777  hauseqlcld  22778  cnextfun  23196  cnextfvval  23197  cnextfres  23201  tgphaus  23249  utop2nei  23383  utop3cls  23384  ucnima  23414  xmeterval  23566  metustid  23691  metustsym  23692  metustexhalf  23693  elbl4  23700  metuel2  23702  isphtpc  24138  ovolfcl  24611  ovollb2lem  24633  ovolctb  24635  ovolshftlem1  24654  ovolscalem1  24658  ovolicc1  24661  ioombl1lem1  24703  ioorf  24718  dyadf  24736  eldv  25043  dvres2  25057  dvef  25125  eltayl  25500  ulmscl  25519  tglngne  26892  tgelrnln  26972  isperp  27054  brbtwn  27248  iswlk  27958  wlkcpr  27976  wlkcomp  27978  wlkeq  27981  wlklenvclwlk  28002  wlklenvclwlkOLD  28003  wlkreslem  28017  clwlkcomp  28126  clwlkcompbp  28129  wlkswwlksf1o  28223  clwlkclwwlkflem  28347  clwlkclwwlkfolem  28350  clwlkclwwlkfo  28352  wlkl0  28710  ex-br  28774  avril1  28806  helloworld  28808  vcex  28919  h2hlm  29321  axhcompl-zf  29339  opeldifid  30917  brabgaf  30927  opabdm  30930  opabrn  30931  fpwrelmap  31047  gsummpt2co  31287  isarchi  31415  fldextfld1  31703  fldextfld2  31704  qtophaus  31765  prsdm  31843  prsrn  31844  acycgr0v  33089  prclisacycgr  33092  mclsax  33510  brtpid1  33644  brtpid2  33645  brtpid3  33646  brtp  33696  dfso2  33701  fundmpss  33719  opelco3  33728  scutval  33973  dmscut  33984  scutf  33985  madeval2  34016  scutfo  34063  pprodss4v  34165  brsset  34170  brtxpsd  34175  sscoid  34194  dffun10  34195  brimg  34218  funpartfun  34224  funpartfv  34226  dfrecs2  34231  dfrdg4  34232  imagesset  34234  fvtransport  34313  brcolinear2  34339  colineardim1  34342  fvray  34422  fvline  34425  eltail  34542  bj-brrelex12ALT  35217  bj-brresdm  35296  brabd0  35297  bj-ideqg  35307  bj-opelidb1ALT  35316  bj-elid7  35321  bj-opelopabid  35337  uncf  35735  uncov  35737  unccur  35739  phpreu  35740  poimirlem26  35782  mblfinlem2  35794  areacirclem5  35848  heiborlem3  35950  heiborlem4  35951  heiborlem6  35953  isrngo  36034  rngoablo2  36046  isdivrngo  36087  brvdif2  36380  brvvdif  36381  elecALTV  36384  inxprnres  36406  ssrel3  36413  brrabga  36455  iss2  36458  brabidgaw  36474  brabidga  36475  brabsb2  36855  eqbrrdv2  36856  cmtvalN  37204  cvrval  37262  undmrnresiss  41165  cnvssco  41167  cotrintab  41175  elimaint  41210  coiun1  41213  elintima  41214  briunov2  41243  brtrclfv2  41288  frege77d  41307  dfhe3  41336  dffrege76  41500  frege97  41521  frege98  41522  frege109  41533  frege110  41534  dffrege115  41539  frege131  41555  frege133  41557  rfovcnvf1od  41565  fsovrfovd  41570  fourierdlem42  43644  ovolval2lem  44135  ovolval4lem2  44142  afveu  44596  fnopafvb  44598  tz6.12-afv  44616  tz6.12-1-afv  44617  aovprc  44631  aovrcl  44632  funressndmafv2rn  44666  tz6.12-afv2  44683  tz6.12-1-afv2  44684  dfatopafv2b  44689  fnopafv2b  44692  dfafv23  44696  sprsymrelfolem2  44897  sprsymrelf  44899  prproropf1olem0  44906  prproropf1olem2  44908  isupwlk  45250  inclfusubc  45377  funcrngcsetc  45508  funcrngcsetcALT  45509  funcringcsetc  45545  rrx2plord  46018  rrx2plordisom  46021  fvconstr  46135  fvconstrn0  46136  fvconstr2  46137  thincciso  46282
  Copyright terms: Public domain W3C validator