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 4797
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 10263 for the specific definition of <). As a wff, relations are true or false. For example, (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩} → 3𝑅9) (ex-br 27591). Often class 𝑅 meets the Rel criteria to be defined in df-rel 5265, and in particular 𝑅 may be a function (see df-fun 6043). 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 7258). (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 4796 . 2 wff 𝐴𝑅𝐵
51, 2cop 4319 . . 3 class 𝐴, 𝐵
65, 3wcel 2131 . 2 wff 𝐴, 𝐵⟩ ∈ 𝑅
74, 6wb 196 1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Colors of variables: wff setvar class
This definition is referenced by:  breq  4798  breq1  4799  breq2  4800  ssbrd  4839  nfbrd  4842  br0  4845  brne0  4846  brun  4847  brin  4848  brdif  4849  brsymdif  4855  opabss  4858  brv  5081  brabsb  5128  brabga  5131  elopabr  5155  rbropapd  5157  epelg  5172  pofun  5195  brxp  5296  bropaex12  5341  brab2a  5343  eqbrriv  5364  eqbrrdv  5366  eqbrrdiv  5367  opeliunxp2  5408  opelco2g  5437  opelco  5441  elcnv2  5447  opelcnvg  5449  brcnvg  5450  dfdm3  5457  dfrn3  5459  elrng  5461  eldm2g  5467  breldm  5476  dmopab  5482  opelrn  5504  elrn  5513  rnopab  5517  brresg  5550  brresOLD  5554  resieq  5557  opelresi  5558  iss  5597  dfres2  5603  restidsing  5608  restidsingOLD  5609  dfima3  5619  elima3  5623  imai  5628  elimasn  5640  elimasni  5642  eliniseg  5644  cotrg  5657  issref  5659  cnvsym  5660  intasym  5661  asymref  5662  asymref2  5663  intirr  5664  codir  5666  qfto  5667  poirr2  5670  xpdifid  5712  sofld  5731  dmsnn0  5750  coiun  5798  coi1  5804  elpredim  5845  elpredg  5847  dffun4  6053  dffun5  6054  funeu2  6067  funopab  6076  funcnvsn  6089  isarep1  6130  fnop  6147  fneu2  6149  brprcneu  6337  dffv3  6340  tz6.12  6364  funopfv  6388  fnopfvb  6390  opabiota  6415  dffv2  6425  fvopab5  6464  funfvbrb  6485  dff3  6527  dff4  6528  f1ompt  6537  idref  6654  foeqcnvco  6710  f1eqcocnv  6711  fliftel  6714  fliftel1  6715  fliftcnv  6716  isof1oopb  6730  f1oiso  6756  ovprc  6838  fnotovb  6850  brabv  6856  oprabv  6860  elrnmpt2res  6931  resiexg  7259  1st2ndbr  7376  brovpreldm  7414  bropopvvv  7415  frxp  7447  xporderlem  7448  cnvimadfsn  7464  opeliunxp2f  7497  brovex  7509  ottpos  7523  dftpos3  7531  dftpos4  7532  tposoprab  7549  wfrfun  7586  wfrlem17  7592  tfrlem7  7640  tfrlem9a  7643  seqomlem2  7707  seqomlem3  7708  seqomlem4  7709  brwitnlem  7748  ercnv  7924  brdifun  7932  swoord1  7934  swoord2  7935  0er  7940  elecg  7944  iiner  7978  brecop  7999  brsdom  8136  brdom2  8143  idssen  8158  xpcomco  8207  omxpenlem  8218  brsdom2  8241  infxpenlem  9018  dcomex  9453  brdom7disj  9537  brdom6disj  9538  fpwwe2lem8  9643  fpwwe2lem9  9644  fpwwe2lem12  9647  dmrecnq  9974  xrlenlt  10287  brintclab  13933  brtrclfv  13934  dfrtrclrec2  13988  rtrclreclem3  13991  relexpindlem  13994  climcau  14592  caucvgb  14601  divides  15176  vdwpc  15878  isstruct  16064  setsstruct2  16090  prdsleval  16331  imasaddfnlem  16382  imasvscafn  16391  invsym2  16616  brcic  16651  ciclcl  16655  cicrcl  16656  cicsym  16657  funcf1  16719  funcixp  16720  funcid  16723  funcco  16724  funcsect  16725  funcinv  16726  funciso  16727  funcoppc  16728  idfucl  16734  cofuval2  16740  cofucl  16741  funcres  16749  funcres2b  16750  funcres2  16751  wunfunc  16752  funcpropd  16753  funcres2c  16754  isfull  16763  isfth  16767  fthsect  16778  fthinv  16779  fthmon  16780  fthepi  16781  ffthiso  16782  fthres2  16785  idffth  16786  cofull  16787  cofth  16788  ressffth  16791  isnat  16800  natixp  16805  nati  16808  elhomai2  16877  homa1  16880  homahom2  16881  eldmcoa  16908  coapm  16914  catcisolem  16949  catciso  16950  1stfcl  17030  2ndfcl  17031  prfcl  17036  evlfcl  17055  curf1cl  17061  curfcl  17065  hofcl  17092  yonedalem1  17105  yonedalem21  17106  yonedalem22  17111  yonffthlem  17115  yoniso  17118  pospo  17166  efgi  18324  efgi2  18330  gsum2d2lem  18564  dmdprd  18589  dprdval  18594  eldprd  18595  dprd2dlem2  18631  dprd2dlem1  18632  dprd2da  18633  dprd2d2  18635  isunit  18849  subrgdvds  18988  opsrtoslem2  19679  lmrcl  21229  lmff  21299  2ndcctbss  21452  2ndcdisj  21453  hausdiag  21642  hauseqlcld  21643  cnextfun  22061  cnextfvval  22062  cnextfres  22066  tgphaus  22113  utop2nei  22247  utop3cls  22248  ucnima  22278  xmeterval  22430  metustid  22552  metustsym  22553  metustexhalf  22554  elbl4  22561  metuel2  22563  isphtpc  22986  ovolfcl  23427  ovollb2lem  23448  ovolctb  23450  ovolshftlem1  23469  ovolscalem1  23473  ovolicc1  23476  ioombl1lem1  23518  ioorf  23533  dyadf  23551  eldv  23853  dvres2  23867  dvef  23934  eltayl  24305  ulmscl  24324  tglngne  25636  tgelrnln  25716  isperp  25798  brbtwn  25970  iswlk  26708  wlkcpr  26726  wlkcomp  26728  wlkeq  26731  wlklenvclwlk  26753  wlkreslem  26768  clwlkcomp  26877  clwlkcompbp  26880  wlkpwwlkf1ouspgr  26980  wlknwwlksnsur  26991  wlkwwlksur  26998  clwlkclwwlkflem  27119  clwlkclwwlkfolem  27122  clwlkclwwlkfo  27124  clwlksfoclwwlkOLD  27209  wlkl0  27520  ex-br  27591  avril1  27622  helloworld  27624  vcex  27734  h2hlm  28138  axhcompl-zf  28156  opeldifid  29711  brabgaf  29719  opabdm  29722  opabrn  29723  fpwrelmap  29809  isarchi  30037  gsummpt2co  30081  qtophaus  30204  prsdm  30261  prsrn  30262  mclsax  31765  brtpid1  31901  brtpid2  31902  brtpid3  31903  brtp  31938  dfso2  31943  dfpo2  31944  fundmpss  31963  opelco3  31975  frrlem5c  32084  scutval  32209  dmscut  32216  scutf  32217  madeval2  32234  pprodss4v  32289  brsset  32294  brtxpsd  32299  sscoid  32318  dffun10  32319  brimg  32342  funpartfun  32348  funpartfv  32350  dfrecs2  32355  dfrdg4  32356  imagesset  32358  fvtransport  32437  brcolinear2  32463  colineardim1  32466  fvray  32546  fvline  32549  eltail  32667  uncf  33693  uncov  33695  unccur  33697  phpreu  33698  poimirlem26  33740  mblfinlem2  33752  areacirclem5  33809  heiborlem3  33917  heiborlem4  33918  heiborlem6  33920  isrngo  34001  rngoablo2  34013  isdivrngo  34054  brvdif2  34342  brvvdif  34343  elecALTV  34346  brresALTV  34348  inxprnres  34376  ssrel3  34383  opelinxp  34426  iss2  34427  brabidga  34443  brabsb2  34643  eqbrrdv2  34644  cmtvalN  34993  cvrval  35051  undmrnresiss  38404  cnvssco  38406  cotrintab  38415  elimaint  38434  coiun1  38438  elintima  38439  briunov2  38468  brtrclfv2  38513  frege77d  38532  dfhe3  38563  dffrege76  38727  frege97  38748  frege98  38749  frege109  38760  frege110  38761  dffrege115  38766  frege131  38782  frege133  38784  rfovcnvf1od  38792  fsovrfovd  38797  fourierdlem42  40861  ovolval2lem  41355  ovolval4lem2  41362  afveu  41731  fnopafvb  41733  tz6.12-afv  41751  tz6.12-1-afv  41752  aovprc  41766  aovrcl  41767  isupwlk  42219  sprsymrelfolem2  42245  sprsymrelf  42247  inclfusubc  42369  funcrngcsetc  42500  funcrngcsetcALT  42501  funcringcsetc  42537
  Copyright terms: Public domain W3C validator