MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-br Unicode version

Definition df-br 4268
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 and (see df-ltxr 9369 for the specific definition of ). As a wff, relations are true or false. For example, (ex-br 23317). Often class meets the Rel criteria to be defined in df-rel 4818, and in particular may be a function (see df-fun 5392). 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 6483). (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
df-br

Detailed syntax breakdown of Definition df-br
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cR . . 3
41, 2, 3wbr 4267 . 2
51, 2cop 3856 . . 3
65, 3wcel 1749 . 2
74, 6wb 178 1
Colors of variables: wff setvar class
This definition is referenced by:  breq  4269  breq1  4270  breq2  4271  ssbrd  4308  nfbrd  4310  br0  4313  brne0  4314  brun  4315  brin  4316  brdif  4317  sbcbr123  4318  opabss  4328  brabsbOLD  4571  brabsb  4573  brabga  4576  epelg  4604  pofun  4628  brxp  4841  brab2a  4859  brab2ga  4883  eqbrriv  4906  eqbrrdv  4908  eqbrrdiv  4909  opeliunxp2  4949  opelco2g  4978  opelco  4982  cnvss  4983  elcnv2  4988  opelcnvg  4990  brcnvg  4991  dfdm3  4998  dfrn3  5000  elrng  5002  eldm2g  5007  breldm  5015  dmopab  5021  opelrn  5042  elrn  5051  rnopab  5055  brres  5088  brresg  5090  resieq  5092  opelresiOLD  5093  opelresi  5094  iss  5126  dfres2  5130  restidsing  5134  dfima3  5144  elima3  5148  imai  5153  elimasn  5166  elimasni  5168  eliniseg  5170  cotr  5182  issref  5183  cnvsym  5184  intasym  5185  asymref  5186  asymref2  5187  intirr  5188  codir  5190  qfto  5191  poirr2  5194  xpdifid  5238  sofld  5258  dmsnn0  5276  coiun  5319  co02  5323  coi1  5325  dffun4  5402  dffun5  5403  funeu2  5415  funopab  5423  funcnvsn  5433  isarep1  5467  fnop  5484  fneu2  5486  brprcneu  5654  dffv3  5657  tz6.12  5677  funopfv  5701  fnopfvb  5703  opabiota  5724  dffv2  5734  fvopab5  5765  funfvbrb  5786  dff3  5826  dff4  5827  f1ompt  5835  idref  5926  foeqcnvco  5966  f1eqcocnv  5967  fliftel  5970  fliftel1  5971  fliftcnv  5972  f1oiso  6010  ovprc  6088  brabv  6102  elrnmpt2res  6174  resiexg  6484  1st2ndbr  6592  bropopvvv  6622  frxp  6651  xporderlem  6652  cnvimadfsn  6668  brovex  6702  isprmpt2  6705  ottpos  6717  dftpos3  6725  dftpos4  6726  tposoprab  6743  tfrlem7  6801  tfrlem9a  6804  seqomlem2  6865  seqomlem3  6866  seqomlem4  6867  0we1  6907  brwitnlem  6908  ercnv  7083  brdifun  7089  swoord1  7091  swoord2  7092  0er  7097  elecg  7100  iiner  7133  brecop  7154  brsdom  7291  brdom2  7298  idssen  7313  xpcomco  7360  omxpenlem  7371  brsdom2  7394  infxpenlem  8127  dcomex  8563  brdom3  8642  brdom7disj  8645  brdom6disj  8646  fpwwe2lem8  8750  fpwwe2lem9  8751  fpwwe2lem12  8754  canthwe  8764  dmrecnq  9083  xrlenlt  9388  climcau  13089  caucvgb  13098  divides  13477  vdwpc  13981  isstruct  14124  prdsleval  14355  imasaddfnlem  14406  imasvscafn  14415  invsym2  14641  funcf1  14716  funcixp  14717  funcid  14720  funcco  14721  funcsect  14722  funcinv  14723  funciso  14724  funcoppc  14725  idfucl  14731  cofuval2  14737  cofucl  14738  funcres  14746  funcres2b  14747  funcres2  14748  wunfunc  14749  funcpropd  14750  funcres2c  14751  isfull  14760  isfth  14764  fthsect  14775  fthinv  14776  fthmon  14777  fthepi  14778  ffthiso  14779  fthres2  14782  idffth  14783  cofull  14784  cofth  14785  ressffth  14788  isnat  14797  natixp  14802  nati  14805  elhomai2  14842  homa1  14845  homahom2  14846  eldmcoa  14873  coapm  14879  catcisolem  14914  catciso  14915  1stfcl  14947  2ndfcl  14948  prfcl  14953  evlfcl  14972  curf1cl  14978  curfcl  14982  hofcl  15009  yonedalem1  15022  yonedalem21  15023  yonedalem22  15028  yonffthlem  15032  yoniso  15035  pospo  15083  efgi  16153  efgi2  16159  gsum2d2lem  16356  dmdprd  16368  dprdval  16370  eldprd  16371  dprd2dlem2  16407  dprd2dlem1  16408  dprd2da  16409  dprd2d2  16411  isunit  16572  subrgdvds  16692  opsrtoslem2  17368  eltopspOLD  18227  tpsexOLD  18228  lmrcl  18539  lmff  18609  2ndcctbss  18763  2ndcdisj  18764  hausdiag  18922  hauseqlcld  18923  cnextfun  19340  cnextfvval  19341  tgphaus  19391  utop2nei  19525  utop3cls  19526  ucnima  19556  xmeterval  19707  metustidOLD  19834  metustid  19835  metustsymOLD  19836  metustsym  19837  metustexhalfOLD  19838  metustexhalf  19839  elbl4  19851  metuel2  19854  isphtpc  20266  ovolfcl  20650  ovollb2lem  20671  ovolctb  20673  ovolshftlem1  20692  ovolscalem1  20696  ovolicc1  20699  ioombl1lem1  20739  ioorf  20753  dyadf  20771  eldv  21073  dvres2  21087  dvef  21152  eltayl  21566  ulmscl  21585  tgelrnln  22763  tghilbert1_1  22770  brbtwn  22824  iswlk  23105  istrl  23115  ispth  23146  isspth  23147  ex-br  23317  avril1  23335  helloworld  23337  isrngo  23544  rngoablo2  23588  isdivrngo  23597  vcex  23637  h2hlm  24061  axhcompl-zf  24079  opabdm  25623  opabrn  25624  fpwrelmap  25713  isarchi  25878  gsummpt2co  25956  prsdm  26053  prsrn  26054  relexpindlem  27043  dfrtrclrec2  27047  rtrclreclem.trans  27050  brtpid1  27079  brtpid2  27080  brtpid3  27081  brtp  27261  dfso2  27266  dfpo2  27267  fundmpss  27279  opelco3  27291  elpredim  27339  elpredg  27341  wfrlem11  27436  frrlem5c  27476  brsymdif  27561  brv  27610  pprodss4v  27617  brsset  27622  brtxpsd  27627  sscoid  27646  dffun10  27647  brimg  27670  funpartfun  27676  funpartfv  27678  dfrdg4  27683  imagesset  27686  fvtransport  27765  brcolinear2  27791  colineardim1  27794  fvray  27874  fvline  27877  mblfinlem2  28100  areacirclem5  28159  eltail  28266  heiborlem3  28383  heiborlem4  28384  heiborlem6  28386  brabsb2  28679  eqbrrdv2  28680  afveu  29733  fnopafvb  29735  tz6.12-afv  29753  tz6.12-1-afv  29754  aovprc  29768  aovrcl  29769  oprabv  29831  wlkcomp  29960  2wlkeq  29962  wlkcpr  29964  wlknwwlknsur  30018  wlkiswwlksur  30025  isclwlk0  30093  clwlkswlks  30097  clwlkcomp  30100  wlkp1lenfislenp  30186  clwlkfoclwwlk  30192  isrgra  30217  isrusgra  30218  gsumX2d2lem  30505  cmtvalN  32293  cvrval  32351
  Copyright terms: Public domain W3C validator