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

Definition df-br 4244
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 ?Error: < ^ This math symbol is not active (i.e. was not declared in this scope). such as " " that compares two classes and , which might ?Error: 1 ^ This math symbol is not active (i.e. was not declared in this scope). ?Error: 2 ^ This math symbol is not active (i.e. was not declared in this scope). be numbers such as 1 and 2 (see df-ltxr 9176 for the specific ?Error: < ^ This math symbol is not active (i.e. was not declared in this scope). definition of ). As a wff, relations are true or false. For ?Error: 2 , 6 >. , <. 3 , 9 >. } -> 3 R 9 ) ^ This math symbol is not active (i.e. was not declared in this scope). example, ( ={<.2,6>.,<.3,9>.}->3 9) (ex-br 21790). ?Error: Rel ^^^ This math symbol is not active (i.e. was not declared in this scope). Often class meets the Rel criteria to be defined in df-rel 4926, and in particular may be a function (see df-fun 5503). 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. (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 4243 . 2
51, 2cop 3844 . . 3
65, 3wcel 1728 . 2
74, 6wb 178 1
Colors of variables: wff set class
This definition is referenced by:  breq  4245  breq1  4246  breq2  4247  ssbrd  4284  nfbrd  4286  br0  4289  brne0  4290  brun  4291  brin  4292  brdif  4293  sbcbr123  4294  opabss  4304  brabsbOLD  4503  brabsb  4505  brabga  4508  epelg  4536  pofun  4560  brxp  4949  brab2a  4967  brab2ga  4991  eqbrriv  5013  eqbrrdv  5015  eqbrrdiv  5016  opeliunxp2  5055  opelco2g  5082  opelco  5086  cnvss  5087  elcnv2  5092  opelcnvg  5094  brcnvg  5095  dfdm3  5102  dfrn3  5104  elrng  5106  eldm2g  5110  breldm  5118  dmopab  5124  opelrn  5145  elrn  5154  rnopab  5158  brres  5196  brresg  5198  resieq  5200  opelresiOLD  5201  opelresi  5202  resiexg  5232  iss  5233  dfres2  5237  dfima3  5250  elima3  5254  imai  5260  elimasn  5273  elimasni  5275  eliniseg  5277  cotr  5290  issref  5291  cnvsym  5292  intasym  5293  asymref  5294  asymref2  5295  intirr  5296  codir  5298  qfto  5299  poirr2  5302  sofld  5362  dmsnn0  5381  coiun  5425  co02  5429  coi1  5431  dffun4  5513  dffun5  5514  funeu2  5525  funopab  5533  funcnvsn  5543  isarep1  5579  fnop  5595  fneu2  5597  brprcneu  5768  dffv3  5771  tz6.12  5791  funopfv  5814  fnopfvb  5816  dffv2  5844  funfvbrb  5891  dff3  5930  dff4  5931  f1ompt  5939  idref  6027  foeqcnvco  6075  f1eqcocnv  6076  fliftel  6079  fliftel1  6080  fliftcnv  6081  f1oiso  6119  ovprc  6156  brabv  6170  1st2ndbr  6446  bropopvvv  6476  frxp  6506  xporderlem  6507  brovex  6524  isprmpt2  6527  ottpos  6539  dftpos3  6547  dftpos4  6548  tposoprab  6565  fvopab5  6584  opabiota  6588  tfrlem9a  6696  seqomlem2  6757  seqomlem3  6758  seqomlem4  6759  0we1  6799  brwitnlem  6800  ercnv  6975  brdifun  6981  swoord1  6983  swoord2  6984  0er  6989  elecg  6992  iiner  7025  brecop  7046  brsdom  7179  brdom2  7186  idssen  7201  xpcomco  7247  omxpenlem  7258  brsdom2  7280  infxpenlem  7946  dcomex  8378  brdom3  8457  brdom7disj  8460  brdom6disj  8461  fpwwe2lem8  8563  fpwwe2lem9  8564  fpwwe2lem12  8567  canthwe  8577  dmrecnq  8896  xrlenlt  9194  climcau  12515  caucvgb  12524  divides  12905  vdwpc  13399  isstruct  13530  prdsleval  13750  imasaddfnlem  13804  imasvscafn  13813  invsym2  14039  funcf1  14114  funcixp  14115  funcid  14118  funcco  14119  funcsect  14120  funcinv  14121  funciso  14122  funcoppc  14123  idfucl  14129  cofuval2  14135  cofucl  14136  funcres  14144  funcres2b  14145  funcres2  14146  wunfunc  14147  funcpropd  14148  funcres2c  14149  isfull  14158  isfth  14162  fthsect  14173  fthinv  14174  fthmon  14175  fthepi  14176  ffthiso  14177  fthres2  14180  idffth  14181  cofull  14182  cofth  14183  ressffth  14186  isnat  14195  natixp  14200  nati  14203  elhomai2  14240  homa1  14243  homahom2  14244  eldmcoa  14271  coapm  14277  catcisolem  14312  catciso  14313  1stfcl  14345  2ndfcl  14346  prfcl  14351  evlfcl  14370  curf1cl  14376  curfcl  14380  hofcl  14407  yonedalem1  14420  yonedalem21  14421  yonedalem22  14426  yonffthlem  14430  yoniso  14433  pospo  14481  efgi  15402  efgi2  15408  gsum2d2lem  15598  dmdprd  15610  dprdval  15612  eldprd  15613  dprd2dlem2  15649  dprd2dlem1  15650  dprd2da  15651  dprd2d2  15653  isunit  15813  subrgdvds  15933  opsrtoslem2  16596  eltopspOLD  17034  tpsexOLD  17035  lmrcl  17346  lmff  17416  2ndcctbss  17569  2ndcdisj  17570  hausdiag  17728  hauseqlcld  17729  cnextfun  18146  cnextfvval  18147  tgphaus  18197  utop2nei  18331  utop3cls  18332  ucnima  18362  xmeterval  18513  metustidOLD  18640  metustid  18641  metustsymOLD  18642  metustsym  18643  metustexhalfOLD  18644  metustexhalf  18645  elbl4  18657  metuel2  18660  isphtpc  19070  ovolfcl  19414  ovollb2lem  19435  ovolctb  19437  ovolshftlem1  19456  ovolscalem1  19460  ovolicc1  19463  ioombl1lem1  19503  ioorf  19516  dyadf  19534  eldv  19836  dvres2  19850  dvef  19915  eltayl  20327  ulmscl  20346  iswlk  21578  istrl  21588  ispth  21619  isspth  21620  ex-br  21790  avril1  21808  helloworld  21810  isrngo  22017  rngoablo2  22061  isdivrngo  22070  vcex  22110  h2hlm  22534  axhcompl-zf  22552  isarchi  24301  opabdm  24730  opabrn  24731  fpwrelmap  24737  relexpindlem  25243  dfrtrclrec2  25247  rtrclreclem.trans  25250  brtpid1  25282  brtpid2  25283  brtpid3  25284  brtp  25476  dfso2  25481  dfpo2  25482  fundmpss  25494  opelco3  25507  elpredim  25555  elpredg  25557  wfrlem11  25652  frrlem5c  25692  brsymdif  25777  brv  25826  pprodss4v  25833  brsset  25838  brtxpsd  25843  sscoid  25862  dffun10  25863  brimg  25886  funpartfun  25892  funpartfv  25894  dfrdg4  25899  imagesset  25902  brbtwn  25942  fvtransport  26070  brcolinear2  26096  colineardim1  26099  fvray  26179  fvline  26182  mblfinlem2  26353  areacirclem5  26407  eltail  26514  heiborlem3  26633  heiborlem4  26634  heiborlem6  26636  brabsb2  26892  eqbrrdv2  26893  afveu  28172  fnopafvb  28174  tz6.12-afv  28192  tz6.12-1-afv  28193  aovprc  28207  aovrcl  28208  oprabv  28267  wlkcomp  28503  2wlkeq  28505  isrgra  28605  isrusgra  28606  cmtvalN  30249  cvrval  30307
  Copyright terms: Public domain W3C validator