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 5059
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 10669 for the specific definition of <). As a wff, relations are true or false. For example, (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩} → 3𝑅9) (ex-br 28138). Often class 𝑅 meets the Rel criteria to be defined in df-rel 5556, and in particular 𝑅 may be a function (see df-fun 6351). 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 7606). (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 5058 . 2 wff 𝐴𝑅𝐵
51, 2cop 4565 . . 3 class 𝐴, 𝐵
65, 3wcel 2105 . 2 wff 𝐴, 𝐵⟩ ∈ 𝑅
74, 6wb 207 1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Colors of variables: wff setvar class
This definition is referenced by:  breq  5060  breq1  5061  breq2  5062  ssbrd  5101  nfbrd  5104  br0  5107  brne0  5108  brun  5109  brin  5110  brdif  5111  brsymdif  5117  opabss  5122  brv  5356  brabsb  5410  brabga  5413  elopabr  5439  rbropapd  5441  brabv  5445  epelg  5460  epelgOLD  5461  pofun  5485  brxp  5595  opelinxp  5625  bropaex12  5636  brab2a  5638  eqbrriv  5658  eqbrrdv  5660  eqbrrdiv  5661  opeliunxp2  5703  opelco2g  5732  opelco  5736  elcnv2  5742  opelcnvg  5745  dfdm3  5752  dfrn3  5754  elrng  5756  eldm2g  5762  breldm  5771  dmopab  5778  opelrn  5807  elrn  5816  rnopab  5820  brres  5854  resieq  5858  opelidres  5859  iss  5897  dfres2  5903  elidinxp  5905  restidsing  5916  dfima3  5926  elima3  5930  imai  5936  elimasn  5948  elimasni  5950  eliniseg  5952  cotrg  5965  idrefALT  5967  cnvsym  5968  intasym  5969  asymref  5970  asymref2  5971  intirr  5972  codir  5974  qfto  5975  poirr2  5978  xpdifid  6019  sofld  6038  dmsnn0  6058  coiun  6103  coi1  6109  elpredim  6154  elpredg  6156  dffun4  6361  dffun5  6362  funeu2  6375  funopab  6384  funcnvsn  6398  isarep1  6436  fnop  6454  fneu2  6456  brprcneu  6656  dffv3  6660  tz6.12  6687  funopfv  6711  fnopfvb  6713  opabiota  6740  dffv2  6750  fvopab5  6793  funfvbrb  6814  dff3  6859  dff4  6860  f1ompt  6868  idref  6901  foeqcnvco  7047  f1eqcocnv  7048  fliftel  7051  fliftel1  7052  fliftcnv  7053  isof1oopb  7067  f1oiso  7093  ovprc  7183  fnotovb  7195  oprabv  7203  elrnmpores  7277  1st2ndbr  7732  brovpreldm  7775  bropopvvv  7776  frxp  7811  xporderlem  7812  cnvimadfsn  7830  opeliunxp2f  7867  brovex  7879  ottpos  7893  dftpos3  7901  dftpos4  7902  tposoprab  7919  wfrfun  7956  wfrlem17  7962  tfrlem7  8010  tfrlem9a  8013  seqomlem2  8078  seqomlem3  8079  seqomlem4  8080  brwitnlem  8123  ercnv  8300  brdifun  8308  swoord1  8310  swoord2  8311  0er  8316  elecg  8322  iiner  8359  brecop  8380  brsdom  8521  brdom2  8528  idssen  8543  xpcomco  8596  omxpenlem  8607  brsdom2  8630  infxpenlem  9428  dcomex  9858  brdom7disj  9942  brdom6disj  9943  fpwwe2lem8  10048  fpwwe2lem9  10049  fpwwe2lem12  10052  dmrecnq  10379  xrlenlt  10695  brintclab  14351  brtrclfv  14352  dfrtrclrec2  14406  rtrclreclem3  14409  relexpindlem  14412  climcau  15017  caucvgb  15026  divides  15599  vdwpc  16306  isstruct  16486  setsstruct2  16511  prdsleval  16740  imasaddfnlem  16791  imasvscafn  16800  invsym2  17023  brcic  17058  ciclcl  17062  cicrcl  17063  cicsym  17064  funcf1  17126  funcixp  17127  funcid  17130  funcco  17131  funcsect  17132  funcinv  17133  funciso  17134  funcoppc  17135  idfucl  17141  cofuval2  17147  cofucl  17148  funcres  17156  funcres2b  17157  funcres2  17158  wunfunc  17159  funcpropd  17160  funcres2c  17161  isfull  17170  isfth  17174  fthsect  17185  fthinv  17186  fthmon  17187  fthepi  17188  ffthiso  17189  fthres2  17192  idffth  17193  cofull  17194  cofth  17195  ressffth  17198  isnat  17207  natixp  17212  nati  17215  elhomai2  17284  homa1  17287  homahom2  17288  eldmcoa  17315  coapm  17321  catcisolem  17356  catciso  17357  1stfcl  17437  2ndfcl  17438  prfcl  17443  evlfcl  17462  curf1cl  17468  curfcl  17472  hofcl  17499  yonedalem1  17512  yonedalem21  17513  yonedalem22  17518  yonffthlem  17522  yoniso  17525  pospo  17573  efgi  18776  efgi2  18782  gsum2d2lem  19024  gsumxp2  19031  dmdprd  19051  dprdval  19056  eldprd  19057  dprd2dlem2  19093  dprd2dlem1  19094  dprd2da  19095  dprd2d2  19097  isunit  19338  subrgdvds  19480  opsrtoslem2  20195  lmrcl  21769  lmff  21839  2ndcctbss  21993  2ndcdisj  21994  hausdiag  22183  hauseqlcld  22184  cnextfun  22602  cnextfvval  22603  cnextfres  22607  tgphaus  22654  utop2nei  22788  utop3cls  22789  ucnima  22819  xmeterval  22971  metustid  23093  metustsym  23094  metustexhalf  23095  elbl4  23102  metuel2  23104  isphtpc  23527  ovolfcl  23996  ovollb2lem  24018  ovolctb  24020  ovolshftlem1  24039  ovolscalem1  24043  ovolicc1  24046  ioombl1lem1  24088  ioorf  24103  dyadf  24121  eldv  24425  dvres2  24439  dvef  24506  eltayl  24877  ulmscl  24896  tglngne  26264  tgelrnln  26344  isperp  26426  brbtwn  26613  iswlk  27320  wlkcpr  27338  wlkcomp  27340  wlkeq  27343  wlklenvclwlk  27364  wlklenvclwlkOLD  27365  wlkreslem  27379  clwlkcomp  27488  clwlkcompbp  27491  wlkswwlksf1o  27585  clwlkclwwlkflem  27710  clwlkclwwlkfolem  27713  clwlkclwwlkfo  27715  wlkl0  28074  ex-br  28138  avril1  28170  helloworld  28172  vcex  28283  h2hlm  28685  axhcompl-zf  28703  opeldifid  30278  brabgaf  30288  opabdm  30291  opabrn  30292  brsnop  30356  fpwrelmap  30396  gsummpt2co  30614  isarchi  30739  fldextfld1  30939  fldextfld2  30940  qtophaus  31000  prsdm  31057  prsrn  31058  acycgr0v  32293  prclisacycgr  32296  mclsax  32714  brtpid1  32849  brtpid2  32850  brtpid3  32851  brtp  32883  dfso2  32888  dfpo2  32889  fundmpss  32907  opelco3  32916  frrlem9  33029  scutval  33163  dmscut  33170  scutf  33171  madeval2  33188  pprodss4v  33243  brsset  33248  brtxpsd  33253  sscoid  33272  dffun10  33273  brimg  33296  funpartfun  33302  funpartfv  33304  dfrecs2  33309  dfrdg4  33310  imagesset  33312  fvtransport  33391  brcolinear2  33417  colineardim1  33420  fvray  33500  fvline  33503  eltail  33620  bj-brrelex12ALT  34254  bj-brresdm  34331  brabd0  34332  bj-ideqg  34342  bj-opelidb1ALT  34351  bj-elid7  34356  uncf  34753  uncov  34755  unccur  34757  phpreu  34758  poimirlem26  34800  mblfinlem2  34812  areacirclem5  34868  heiborlem3  34974  heiborlem4  34975  heiborlem6  34977  isrngo  35058  rngoablo2  35070  isdivrngo  35111  brvdif2  35406  brvvdif  35407  elecALTV  35410  inxprnres  35432  ssrel3  35439  brrabga  35481  iss2  35484  brabidga  35500  brabsb2  35880  eqbrrdv2  35881  cmtvalN  36229  cvrval  36287  undmrnresiss  39844  cnvssco  39846  cotrintab  39854  elimaint  39873  coiun1  39877  elintima  39878  briunov2  39907  brtrclfv2  39952  frege77d  39971  dfhe3  40001  dffrege76  40165  frege97  40186  frege98  40187  frege109  40198  frege110  40199  dffrege115  40204  frege131  40220  frege133  40222  rfovcnvf1od  40230  fsovrfovd  40235  fourierdlem42  42315  ovolval2lem  42806  ovolval4lem2  42813  afveu  43233  fnopafvb  43235  tz6.12-afv  43253  tz6.12-1-afv  43254  aovprc  43268  aovrcl  43269  funressndmafv2rn  43303  tz6.12-afv2  43320  tz6.12-1-afv2  43321  dfatopafv2b  43326  fnopafv2b  43329  dfafv23  43333  sprsymrelfolem2  43502  sprsymrelf  43504  prproropf1olem0  43511  prproropf1olem2  43513  isupwlk  43858  inclfusubc  44036  funcrngcsetc  44167  funcrngcsetcALT  44168  funcringcsetc  44204  rrx2plord  44605  rrx2plordisom  44608
  Copyright terms: Public domain W3C validator