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 4928
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 10475 for the specific definition of <). As a wff, relations are true or false. For example, (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩} → 3𝑅9) (ex-br 27982). Often class 𝑅 meets the Rel criteria to be defined in df-rel 5411, and in particular 𝑅 may be a function (see df-fun 6188). 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 7431). (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 4927 . 2 wff 𝐴𝑅𝐵
51, 2cop 4445 . . 3 class 𝐴, 𝐵
65, 3wcel 2048 . 2 wff 𝐴, 𝐵⟩ ∈ 𝑅
74, 6wb 198 1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Colors of variables: wff setvar class
This definition is referenced by:  breq  4929  breq1  4930  breq2  4931  ssbrd  4970  nfbrd  4973  br0  4976  brne0  4977  brun  4978  brin  4979  brdif  4980  brsymdif  4986  opabss  4991  brv  5218  brabsb  5269  brabga  5272  elopabr  5296  rbropapd  5298  brabv  5302  epelg  5315  epelgOLD  5316  pofun  5340  brxp  5450  opelinxp  5478  bropaex12  5489  brab2a  5491  eqbrriv  5511  eqbrrdv  5513  eqbrrdiv  5514  opeliunxp2  5556  opelco2g  5585  opelco  5589  elcnv2  5595  opelcnvg  5598  dfdm3  5605  dfrn3  5607  elrng  5609  eldm2g  5615  breldm  5624  dmopab  5630  opelrn  5653  elrn  5662  rnopab  5666  brres  5699  brresgOLD2  5703  resieq  5707  opelidres  5708  iss  5746  dfres2  5752  elidinxp  5754  restidsing  5762  dfima3  5771  elima3  5775  imai  5780  elimasn  5792  elimasni  5794  eliniseg  5796  cotrg  5809  idrefALT  5811  cnvsym  5812  intasym  5813  asymref  5814  asymref2  5815  intirr  5816  codir  5818  qfto  5819  poirr2  5822  xpdifid  5863  sofld  5882  dmsnn0  5901  coiun  5946  coi1  5952  elpredim  5996  elpredg  5998  dffun4  6198  dffun5  6199  funeu2  6212  funopab  6221  funcnvsn  6235  isarep1  6273  fnop  6291  fneu2  6293  brprcneu  6489  dffv3  6493  tz6.12  6520  funopfv  6545  fnopfvb  6547  opabiota  6572  dffv2  6582  fvopab5  6623  funfvbrb  6644  dff3  6687  dff4  6688  f1ompt  6696  idref  6729  foeqcnvco  6879  f1eqcocnv  6880  fliftel  6883  fliftel1  6884  fliftcnv  6885  isof1oopb  6899  f1oiso  6925  ovprc  7011  fnotovb  7023  oprabv  7031  elrnmpores  7102  1st2ndbr  7550  brovpreldm  7589  bropopvvv  7590  frxp  7622  xporderlem  7623  cnvimadfsn  7639  opeliunxp2f  7676  brovex  7688  ottpos  7702  dftpos3  7710  dftpos4  7711  tposoprab  7728  wfrfun  7766  wfrlem17  7772  tfrlem7  7820  tfrlem9a  7823  seqomlem2  7887  seqomlem3  7888  seqomlem4  7889  brwitnlem  7930  ercnv  8106  brdifun  8114  swoord1  8116  swoord2  8117  0er  8122  elecg  8128  iiner  8165  brecop  8186  brsdom  8325  brdom2  8332  idssen  8347  xpcomco  8399  omxpenlem  8410  brsdom2  8433  infxpenlem  9229  dcomex  9663  brdom7disj  9747  brdom6disj  9748  fpwwe2lem8  9853  fpwwe2lem9  9854  fpwwe2lem12  9857  dmrecnq  10184  xrlenlt  10502  brintclab  14216  brtrclfv  14217  dfrtrclrec2  14271  rtrclreclem3  14274  relexpindlem  14277  climcau  14882  caucvgb  14891  divides  15463  vdwpc  16166  isstruct  16346  setsstruct2  16371  prdsleval  16600  imasaddfnlem  16651  imasvscafn  16660  invsym2  16885  brcic  16920  ciclcl  16924  cicrcl  16925  cicsym  16926  funcf1  16988  funcixp  16989  funcid  16992  funcco  16993  funcsect  16994  funcinv  16995  funciso  16996  funcoppc  16997  idfucl  17003  cofuval2  17009  cofucl  17010  funcres  17018  funcres2b  17019  funcres2  17020  wunfunc  17021  funcpropd  17022  funcres2c  17023  isfull  17032  isfth  17036  fthsect  17047  fthinv  17048  fthmon  17049  fthepi  17050  ffthiso  17051  fthres2  17054  idffth  17055  cofull  17056  cofth  17057  ressffth  17060  isnat  17069  natixp  17074  nati  17077  elhomai2  17146  homa1  17149  homahom2  17150  eldmcoa  17177  coapm  17183  catcisolem  17218  catciso  17219  1stfcl  17299  2ndfcl  17300  prfcl  17305  evlfcl  17324  curf1cl  17330  curfcl  17334  hofcl  17361  yonedalem1  17374  yonedalem21  17375  yonedalem22  17380  yonffthlem  17384  yoniso  17387  pospo  17435  efgi  18597  efgi2  18603  gsum2d2lem  18840  dmdprd  18864  dprdval  18869  eldprd  18870  dprd2dlem2  18906  dprd2dlem1  18907  dprd2da  18908  dprd2d2  18910  isunit  19124  subrgdvds  19266  opsrtoslem2  19972  lmrcl  21537  lmff  21607  2ndcctbss  21761  2ndcdisj  21762  hausdiag  21951  hauseqlcld  21952  cnextfun  22370  cnextfvval  22371  cnextfres  22375  tgphaus  22422  utop2nei  22556  utop3cls  22557  ucnima  22587  xmeterval  22739  metustid  22861  metustsym  22862  metustexhalf  22863  elbl4  22870  metuel2  22872  isphtpc  23295  ovolfcl  23764  ovollb2lem  23786  ovolctb  23788  ovolshftlem1  23807  ovolscalem1  23811  ovolicc1  23814  ioombl1lem1  23856  ioorf  23871  dyadf  23889  eldv  24193  dvres2  24207  dvef  24274  eltayl  24645  ulmscl  24664  tglngne  26032  tgelrnln  26112  isperp  26194  brbtwn  26382  iswlk  27089  wlkcpr  27107  wlkcomp  27109  wlkeq  27112  wlklenvclwlk  27133  wlkreslem  27149  wlkreslemOLD  27151  clwlkcomp  27262  clwlkcompbp  27265  wlkswwlksf1o  27359  clwlkclwwlkflem  27506  clwlkclwwlkfolem  27511  clwlkclwwlkfoOLD  27513  clwlkclwwlkfo  27517  wlkl0  27914  ex-br  27982  avril1  28013  helloworld  28015  vcex  28126  h2hlm  28530  axhcompl-zf  28548  opeldifid  30109  brabgaf  30117  opabdm  30120  opabrn  30121  fpwrelmap  30215  isarchi  30468  gsummpt2co  30514  fldextfld1  30659  fldextfld2  30660  qtophaus  30735  prsdm  30792  prsrn  30793  mclsax  32306  brtpid1  32441  brtpid2  32442  brtpid3  32443  brtp  32475  dfso2  32480  dfpo2  32481  fundmpss  32499  opelco3  32508  frrlem9  32622  scutval  32756  dmscut  32763  scutf  32764  madeval2  32781  pprodss4v  32836  brsset  32841  brtxpsd  32846  sscoid  32865  dffun10  32866  brimg  32889  funpartfun  32895  funpartfv  32897  dfrecs2  32902  dfrdg4  32903  imagesset  32905  fvtransport  32984  brcolinear2  33010  colineardim1  33013  fvray  33093  fvline  33096  eltail  33213  bj-brrelex12ALT  33833  uncf  34290  uncov  34292  unccur  34294  phpreu  34295  poimirlem26  34337  mblfinlem2  34349  areacirclem5  34405  heiborlem3  34511  heiborlem4  34512  heiborlem6  34514  isrngo  34595  rngoablo2  34607  isdivrngo  34648  brvdif2  34945  brvvdif  34946  elecALTV  34949  inxprnres  34971  ssrel3  34978  brrabga  35022  iss2  35025  brabidga  35041  brabsb2  35421  eqbrrdv2  35422  cmtvalN  35770  cvrval  35828  undmrnresiss  39304  cnvssco  39306  cotrintab  39315  elimaint  39334  coiun1  39338  elintima  39339  briunov2  39368  brtrclfv2  39413  frege77d  39432  dfhe3  39462  dffrege76  39626  frege97  39647  frege98  39648  frege109  39659  frege110  39660  dffrege115  39665  frege131  39681  frege133  39683  rfovcnvf1od  39691  fsovrfovd  39696  fourierdlem42  41844  ovolval2lem  42335  ovolval4lem2  42342  afveu  42737  fnopafvb  42739  tz6.12-afv  42757  tz6.12-1-afv  42758  aovprc  42772  aovrcl  42773  funressndmafv2rn  42807  tz6.12-afv2  42824  tz6.12-1-afv2  42825  dfatopafv2b  42830  fnopafv2b  42833  dfafv23  42837  sprsymrelfolem2  42997  sprsymrelf  42999  prproropf1olem0  43006  prproropf1olem2  43008  isupwlk  43353  inclfusubc  43476  funcrngcsetc  43607  funcrngcsetcALT  43608  funcringcsetc  43644  rrx2plord  44049  rrx2plordisom  44052
  Copyright terms: Public domain W3C validator