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 4624
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 10039 for the specific definition of <). As a wff, relations are true or false. For example, (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩} → 3𝑅9) (ex-br 27176). Often class 𝑅 meets the Rel criteria to be defined in df-rel 5091, and in particular 𝑅 may be a function (see df-fun 5859). 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 7063). (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 4623 . 2 wff 𝐴𝑅𝐵
51, 2cop 4161 . . 3 class 𝐴, 𝐵
65, 3wcel 1987 . 2 wff 𝐴, 𝐵⟩ ∈ 𝑅
74, 6wb 196 1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Colors of variables: wff setvar class
This definition is referenced by:  breq  4625  breq1  4626  breq2  4627  ssbrd  4666  nfbrd  4668  br0  4671  brne0  4672  brun  4673  brin  4674  brdif  4675  brsymdif  4681  opabss  4686  brabsb  4956  brabga  4959  elopabr  4983  rbropapd  4985  epelg  4996  pofun  5021  brxp  5117  brab2a  5139  bropaex12  5163  brab2ga  5165  eqbrriv  5186  eqbrrdv  5188  eqbrrdiv  5189  opeliunxp2  5230  opelco2g  5259  opelco  5263  cnvssOLD  5265  elcnv2  5270  opelcnvg  5272  brcnvg  5273  dfdm3  5280  dfrn3  5282  elrng  5284  eldm2g  5290  breldm  5299  dmopab  5305  opelrn  5327  elrn  5336  rnopab  5340  brres  5372  brresg  5374  resieq  5376  opelresi  5377  iss  5416  dfres2  5422  restidsing  5427  restidsingOLD  5428  dfima3  5438  elima3  5442  imai  5447  elimasn  5459  elimasni  5461  eliniseg  5463  cotrg  5476  issref  5478  cnvsym  5479  intasym  5480  asymref  5481  asymref2  5482  intirr  5483  codir  5485  qfto  5486  poirr2  5489  xpdifid  5531  sofld  5550  dmsnn0  5569  coiun  5614  coi1  5620  elpredim  5661  elpredg  5663  dffun4  5869  dffun5  5870  funeu2  5883  funopab  5891  funcnvsn  5904  isarep1  5945  fnop  5962  fneu2  5964  brprcneu  6151  dffv3  6154  tz6.12  6178  funopfv  6202  fnopfvb  6204  opabiota  6228  dffv2  6238  fvopab5  6275  funfvbrb  6296  dff3  6338  dff4  6339  f1ompt  6348  idref  6464  foeqcnvco  6520  f1eqcocnv  6521  fliftel  6524  fliftel1  6525  fliftcnv  6526  isof1oopb  6540  f1oiso  6566  ovprc  6648  brabv  6664  oprabv  6668  elrnmpt2res  6739  resiexg  7064  1st2ndbr  7177  brovpreldm  7214  bropopvvv  7215  frxp  7247  xporderlem  7248  cnvimadfsn  7264  opeliunxp2f  7296  brovex  7308  ottpos  7322  dftpos3  7330  dftpos4  7331  tposoprab  7348  wfrfun  7385  wfrlem17  7391  tfrlem7  7439  tfrlem9a  7442  seqomlem2  7506  seqomlem3  7507  seqomlem4  7508  brwitnlem  7547  ercnv  7723  brdifun  7731  swoord1  7733  swoord2  7734  0er  7740  0erOLD  7741  elecg  7745  iiner  7779  brecop  7800  brsdom  7938  brdom2  7945  idssen  7960  xpcomco  8010  omxpenlem  8021  brsdom2  8044  infxpenlem  8796  dcomex  9229  brdom7disj  9313  brdom6disj  9314  fpwwe2lem8  9419  fpwwe2lem9  9420  fpwwe2lem12  9423  dmrecnq  9750  xrlenlt  10063  brintclab  13692  brtrclfv  13693  dfrtrclrec2  13747  rtrclreclem3  13750  relexpindlem  13753  climcau  14351  caucvgb  14360  divides  14928  vdwpc  15627  isstruct  15812  setsstruct2  15836  prdsleval  16077  imasaddfnlem  16128  imasvscafn  16137  invsym2  16363  brcic  16398  ciclcl  16402  cicrcl  16403  cicsym  16404  funcf1  16466  funcixp  16467  funcid  16470  funcco  16471  funcsect  16472  funcinv  16473  funciso  16474  funcoppc  16475  idfucl  16481  cofuval2  16487  cofucl  16488  funcres  16496  funcres2b  16497  funcres2  16498  wunfunc  16499  funcpropd  16500  funcres2c  16501  isfull  16510  isfth  16514  fthsect  16525  fthinv  16526  fthmon  16527  fthepi  16528  ffthiso  16529  fthres2  16532  idffth  16533  cofull  16534  cofth  16535  ressffth  16538  isnat  16547  natixp  16552  nati  16555  elhomai2  16624  homa1  16627  homahom2  16628  eldmcoa  16655  coapm  16661  catcisolem  16696  catciso  16697  1stfcl  16777  2ndfcl  16778  prfcl  16783  evlfcl  16802  curf1cl  16808  curfcl  16812  hofcl  16839  yonedalem1  16852  yonedalem21  16853  yonedalem22  16858  yonffthlem  16862  yoniso  16865  pospo  16913  efgi  18072  efgi2  18078  gsum2d2lem  18312  dmdprd  18337  dprdval  18342  eldprd  18343  dprd2dlem2  18379  dprd2dlem1  18380  dprd2da  18381  dprd2d2  18383  isunit  18597  subrgdvds  18734  opsrtoslem2  19425  lmrcl  20975  lmff  21045  2ndcctbss  21198  2ndcdisj  21199  hausdiag  21388  hauseqlcld  21389  cnextfun  21808  cnextfvval  21809  cnextfres  21813  tgphaus  21860  utop2nei  21994  utop3cls  21995  ucnima  22025  xmeterval  22177  metustid  22299  metustsym  22300  metustexhalf  22301  elbl4  22308  metuel2  22310  isphtpc  22733  ovolfcl  23175  ovollb2lem  23196  ovolctb  23198  ovolshftlem1  23217  ovolscalem1  23221  ovolicc1  23224  ioombl1lem1  23266  ioorf  23281  dyadf  23299  eldv  23602  dvres2  23616  dvef  23681  eltayl  24052  ulmscl  24071  tglngne  25379  tgelrnln  25459  isperp  25541  brbtwn  25713  iswlk  26410  wlkcpr  26428  wlkcomp  26430  wlkeq  26433  wlklenvclwlk  26454  wlkreslem  26469  clwlkcomp  26578  wlkpwwlkf1ouspgr  26668  wlknwwlksnsur  26679  wlkwwlksur  26686  clwlksfoclwwlk  26863  ex-br  27176  avril1  27207  helloworld  27209  vcex  27321  h2hlm  27725  axhcompl-zf  27743  opeldifid  29298  brabgaf  29304  opabdm  29307  opabrn  29308  fpwrelmap  29392  isarchi  29563  gsummpt2co  29607  qtophaus  29727  prsdm  29784  prsrn  29785  mclsax  31227  brtpid1  31364  brtpid2  31365  brtpid3  31366  brtp  31400  dfso2  31405  dfpo2  31406  fundmpss  31421  opelco3  31433  frrlem5c  31540  brv  31679  pprodss4v  31686  brsset  31691  brtxpsd  31696  sscoid  31715  dffun10  31716  brimg  31739  funpartfun  31745  funpartfv  31747  dfrecs2  31752  dfrdg4  31753  imagesset  31755  fvtransport  31834  brcolinear2  31860  colineardim1  31863  fvray  31943  fvline  31946  eltail  32064  uncf  33059  uncov  33061  unccur  33063  phpreu  33064  poimirlem26  33106  mblfinlem2  33118  areacirclem5  33175  heiborlem3  33283  heiborlem4  33284  heiborlem6  33286  isrngo  33367  rngoablo2  33379  isdivrngo  33420  brabsb2  33666  eqbrrdv2  33667  cmtvalN  34017  cvrval  34075  undmrnresiss  37430  cnvssco  37432  cotrintab  37441  elimaint  37460  coiun1  37464  elintima  37465  briunov2  37494  brtrclfv2  37539  frege77d  37558  dfhe3  37590  dffrege76  37754  frege97  37775  frege98  37776  frege109  37787  frege110  37788  dffrege115  37793  frege131  37809  frege133  37811  rfovcnvf1od  37819  fsovrfovd  37824  fourierdlem42  39703  ovolval2lem  40194  ovolval4lem2  40201  afveu  40567  fnopafvb  40569  tz6.12-afv  40587  tz6.12-1-afv  40588  aovprc  40602  aovrcl  40603  isupwlk  41035  sprsymrelfolem2  41061  sprsymrelf  41063  inclfusubc  41185  funcrngcsetc  41316  funcrngcsetcALT  41317  funcringcsetc  41353
  Copyright terms: Public domain W3C validator