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 4584
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 9958 for the specific definition of <). As a wff, relations are true or false. For example, (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩} → 3𝑅9) (ex-br 26680). Often class 𝑅 meets the Rel criteria to be defined in df-rel 5045, and in particular 𝑅 may be a function (see df-fun 5806). 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 6993). (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 4583 . 2 wff 𝐴𝑅𝐵
51, 2cop 4131 . . 3 class 𝐴, 𝐵
65, 3wcel 1977 . 2 wff 𝐴, 𝐵⟩ ∈ 𝑅
74, 6wb 195 1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Colors of variables: wff setvar class
This definition is referenced by:  breq  4585  breq1  4586  breq2  4587  ssbrd  4626  nfbrd  4628  br0  4631  brne0  4632  brun  4633  brin  4634  brdif  4635  brsymdif  4641  opabss  4646  brabsb  4911  brabga  4914  elopabr  4937  rbropapd  4939  epelg  4950  pofun  4975  brxp  5071  brab2a  5091  bropaex12  5115  brab2ga  5117  eqbrriv  5138  eqbrrdv  5140  eqbrrdiv  5141  opeliunxp2  5182  opelco2g  5211  opelco  5215  cnvssOLD  5217  elcnv2  5222  opelcnvg  5224  brcnvg  5225  dfdm3  5232  dfrn3  5234  elrng  5236  eldm2g  5242  breldm  5251  dmopab  5257  opelrn  5278  elrn  5287  rnopab  5291  brres  5323  brresg  5325  resieq  5327  opelresi  5328  iss  5367  dfres2  5372  restidsing  5377  restidsingOLD  5378  dfima3  5388  elima3  5392  imai  5397  elimasn  5409  elimasni  5411  eliniseg  5413  cotrg  5426  issref  5428  cnvsym  5429  intasym  5430  asymref  5431  asymref2  5432  intirr  5433  codir  5435  qfto  5436  poirr2  5439  xpdifid  5481  sofld  5500  dmsnn0  5518  coiun  5562  coi1  5568  elpredim  5609  elpredg  5611  dffun4  5816  dffun5  5817  funeu2  5829  funopab  5837  funcnvsn  5850  isarep1  5891  fnop  5908  fneu2  5910  brprcneu  6096  dffv3  6099  tz6.12  6121  funopfv  6145  fnopfvb  6147  opabiota  6171  dffv2  6181  fvopab5  6217  funfvbrb  6238  dff3  6280  dff4  6281  f1ompt  6290  idref  6403  foeqcnvco  6455  f1eqcocnv  6456  fliftel  6459  fliftel1  6460  fliftcnv  6461  isof1oopb  6475  f1oiso  6501  ovprc  6581  brabv  6597  oprabv  6601  elrnmpt2res  6672  resiexg  6994  1st2ndbr  7108  brovpreldm  7141  bropopvvv  7142  frxp  7174  xporderlem  7175  cnvimadfsn  7191  opeliunxp2f  7223  brovex  7235  ottpos  7249  dftpos3  7257  dftpos4  7258  tposoprab  7275  wfrfun  7312  wfrlem17  7318  tfrlem7  7366  tfrlem9a  7369  seqomlem2  7433  seqomlem3  7434  seqomlem4  7435  brwitnlem  7474  ercnv  7650  brdifun  7658  swoord1  7660  swoord2  7661  0er  7667  0erOLD  7668  elecg  7672  iiner  7706  brecop  7727  brsdom  7864  brdom2  7871  idssen  7886  xpcomco  7935  omxpenlem  7946  brsdom2  7969  infxpenlem  8719  dcomex  9152  brdom7disj  9234  brdom6disj  9235  fpwwe2lem8  9338  fpwwe2lem9  9339  fpwwe2lem12  9342  dmrecnq  9669  xrlenlt  9982  brintclab  13590  brtrclfv  13591  dfrtrclrec2  13645  rtrclreclem3  13648  relexpindlem  13651  climcau  14249  caucvgb  14258  divides  14823  vdwpc  15522  isstruct  15705  prdsleval  15960  imasaddfnlem  16011  imasvscafn  16020  invsym2  16246  brcic  16281  ciclcl  16285  cicrcl  16286  cicsym  16287  funcf1  16349  funcixp  16350  funcid  16353  funcco  16354  funcsect  16355  funcinv  16356  funciso  16357  funcoppc  16358  idfucl  16364  cofuval2  16370  cofucl  16371  funcres  16379  funcres2b  16380  funcres2  16381  wunfunc  16382  funcpropd  16383  funcres2c  16384  isfull  16393  isfth  16397  fthsect  16408  fthinv  16409  fthmon  16410  fthepi  16411  ffthiso  16412  fthres2  16415  idffth  16416  cofull  16417  cofth  16418  ressffth  16421  isnat  16430  natixp  16435  nati  16438  elhomai2  16507  homa1  16510  homahom2  16511  eldmcoa  16538  coapm  16544  catcisolem  16579  catciso  16580  1stfcl  16660  2ndfcl  16661  prfcl  16666  evlfcl  16685  curf1cl  16691  curfcl  16695  hofcl  16722  yonedalem1  16735  yonedalem21  16736  yonedalem22  16741  yonffthlem  16745  yoniso  16748  pospo  16796  efgi  17955  efgi2  17961  gsum2d2lem  18195  dmdprd  18220  dprdval  18225  eldprd  18226  dprd2dlem2  18262  dprd2dlem1  18263  dprd2da  18264  dprd2d2  18266  isunit  18480  subrgdvds  18617  opsrtoslem2  19306  lmrcl  20845  lmff  20915  2ndcctbss  21068  2ndcdisj  21069  hausdiag  21258  hauseqlcld  21259  cnextfun  21678  cnextfvval  21679  cnextfres  21683  tgphaus  21730  utop2nei  21864  utop3cls  21865  ucnima  21895  xmeterval  22047  metustid  22169  metustsym  22170  metustexhalf  22171  elbl4  22178  metuel2  22180  isphtpc  22601  ovolfcl  23042  ovollb2lem  23063  ovolctb  23065  ovolshftlem1  23084  ovolscalem1  23088  ovolicc1  23091  ioombl1lem1  23133  ioorf  23147  dyadf  23165  eldv  23468  dvres2  23482  dvef  23547  eltayl  23918  ulmscl  23937  tglngne  25245  tgelrnln  25325  isperp  25407  brbtwn  25579  uhgraop  25833  usgrac  25880  elusuhgra  25897  usgraexmplc  25933  iswlk  26048  wlkcomp  26053  wlkcpr  26057  istrl  26067  ispth  26098  isspth  26099  2wlkeq  26235  wlknwwlknsur  26240  wlkiswwlksur  26247  isclwlk0  26282  clwlkswlks  26286  clwlkcomp  26291  wlklenvclwlk  26366  clwlkfoclwwlk  26372  isrgra  26453  isrusgra  26454  isrusgusrgcl  26460  0eusgraiff0rgracl  26468  ex-br  26680  avril1  26711  helloworld  26713  vcex  26817  h2hlm  27221  axhcompl-zf  27239  opeldifid  28794  brabgaf  28800  opabdm  28803  opabrn  28804  fpwrelmap  28896  isarchi  29067  gsummpt2co  29111  qtophaus  29231  prsdm  29288  prsrn  29289  mclsax  30720  brtpid1  30857  brtpid2  30858  brtpid3  30859  brtp  30892  dfso2  30897  dfpo2  30898  fundmpss  30910  opelco3  30923  frrlem5c  31030  brv  31154  pprodss4v  31161  brsset  31166  brtxpsd  31171  sscoid  31190  dffun10  31191  brimg  31214  funpartfun  31220  funpartfv  31222  dfrecs2  31227  dfrdg4  31228  imagesset  31230  fvtransport  31309  brcolinear2  31335  colineardim1  31338  fvray  31418  fvline  31421  eltail  31539  uncf  32558  uncov  32560  unccur  32562  phpreu  32563  poimirlem26  32605  mblfinlem2  32617  areacirclem5  32674  heiborlem3  32782  heiborlem4  32783  heiborlem6  32785  isrngo  32866  rngoablo2  32878  isdivrngo  32919  brabsb2  33165  eqbrrdv2  33166  cmtvalN  33516  cvrval  33574  undmrnresiss  36929  cnvssco  36931  cotrintab  36940  elimaint  36959  coiun1  36963  elintima  36964  briunov2  36993  brtrclfv2  37038  frege77d  37057  dfhe3  37089  dffrege76  37253  frege97  37274  frege98  37275  frege109  37286  frege110  37287  dffrege115  37292  frege131  37308  frege133  37310  rfovcnvf1od  37318  fsovrfovd  37323  fourierdlem42  39042  ovolval2lem  39533  ovolval4lem2  39540  afveu  39882  fnopafvb  39884  tz6.12-afv  39902  tz6.12-1-afv  39903  aovprc  39917  aovrcl  39918  is1wlk  40813  isWlk  40814  1wlkcpr  40833  1wlkcomp  40835  1wlkeq  40838  1wlklenvclwlk  40863  1wlkreslem  40878  clWlkcomp  40986  1wlkpwwlkf1ouspgr  41076  wlknwwlksnsur  41087  wlkwwlksur  41094  clwlksfoclwwlk  41270  inclfusubc  41657  funcrngcsetc  41790  funcrngcsetcALT  41791  funcringcsetc  41827
  Copyright terms: Public domain W3C validator