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 4686
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 10117 for the specific definition of <). As a wff, relations are true or false. For example, (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩} → 3𝑅9) (ex-br 27418). Often class 𝑅 meets the Rel criteria to be defined in df-rel 5150, and in particular 𝑅 may be a function (see df-fun 5928). 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 7143). (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 4685 . 2 wff 𝐴𝑅𝐵
51, 2cop 4216 . . 3 class 𝐴, 𝐵
65, 3wcel 2030 . 2 wff 𝐴, 𝐵⟩ ∈ 𝑅
74, 6wb 196 1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Colors of variables: wff setvar class
This definition is referenced by:  breq  4687  breq1  4688  breq2  4689  ssbrd  4728  nfbrd  4731  br0  4734  brne0  4735  brun  4736  brin  4737  brdif  4738  brsymdif  4744  opabss  4747  brv  4970  brabsb  5015  brabga  5018  elopabr  5042  rbropapd  5044  epelg  5059  pofun  5080  brxp  5181  bropaex12  5226  brab2a  5228  eqbrriv  5249  eqbrrdv  5251  eqbrrdiv  5252  opeliunxp2  5293  opelco2g  5322  opelco  5326  elcnv2  5332  opelcnvg  5334  brcnvg  5335  dfdm3  5342  dfrn3  5344  elrng  5346  eldm2g  5352  breldm  5361  dmopab  5367  opelrn  5389  elrn  5398  rnopab  5402  brresg  5435  brresOLD  5439  resieq  5442  opelresi  5443  iss  5482  dfres2  5488  restidsing  5493  restidsingOLD  5494  dfima3  5504  elima3  5508  imai  5513  elimasn  5525  elimasni  5527  eliniseg  5529  cotrg  5542  issref  5544  cnvsym  5545  intasym  5546  asymref  5547  asymref2  5548  intirr  5549  codir  5551  qfto  5552  poirr2  5555  xpdifid  5597  sofld  5616  dmsnn0  5635  coiun  5683  coi1  5689  elpredim  5730  elpredg  5732  dffun4  5938  dffun5  5939  funeu2  5952  funopab  5961  funcnvsn  5974  isarep1  6015  fnop  6032  fneu2  6034  brprcneu  6222  dffv3  6225  tz6.12  6249  funopfv  6273  fnopfvb  6275  opabiota  6300  dffv2  6310  fvopab5  6349  funfvbrb  6370  dff3  6412  dff4  6413  f1ompt  6422  idref  6539  foeqcnvco  6595  f1eqcocnv  6596  fliftel  6599  fliftel1  6600  fliftcnv  6601  isof1oopb  6615  f1oiso  6641  ovprc  6723  fnotovb  6735  brabv  6741  oprabv  6745  elrnmpt2res  6816  resiexg  7144  1st2ndbr  7261  brovpreldm  7299  bropopvvv  7300  frxp  7332  xporderlem  7333  cnvimadfsn  7349  opeliunxp2f  7381  brovex  7393  ottpos  7407  dftpos3  7415  dftpos4  7416  tposoprab  7433  wfrfun  7470  wfrlem17  7476  tfrlem7  7524  tfrlem9a  7527  seqomlem2  7591  seqomlem3  7592  seqomlem4  7593  brwitnlem  7632  ercnv  7808  brdifun  7816  swoord1  7818  swoord2  7819  0er  7824  elecg  7828  iiner  7862  brecop  7883  brsdom  8020  brdom2  8027  idssen  8042  xpcomco  8091  omxpenlem  8102  brsdom2  8125  infxpenlem  8874  dcomex  9307  brdom7disj  9391  brdom6disj  9392  fpwwe2lem8  9497  fpwwe2lem9  9498  fpwwe2lem12  9501  dmrecnq  9828  xrlenlt  10141  brintclab  13786  brtrclfv  13787  dfrtrclrec2  13841  rtrclreclem3  13844  relexpindlem  13847  climcau  14445  caucvgb  14454  divides  15029  vdwpc  15731  isstruct  15917  setsstruct2  15943  prdsleval  16184  imasaddfnlem  16235  imasvscafn  16244  invsym2  16470  brcic  16505  ciclcl  16509  cicrcl  16510  cicsym  16511  funcf1  16573  funcixp  16574  funcid  16577  funcco  16578  funcsect  16579  funcinv  16580  funciso  16581  funcoppc  16582  idfucl  16588  cofuval2  16594  cofucl  16595  funcres  16603  funcres2b  16604  funcres2  16605  wunfunc  16606  funcpropd  16607  funcres2c  16608  isfull  16617  isfth  16621  fthsect  16632  fthinv  16633  fthmon  16634  fthepi  16635  ffthiso  16636  fthres2  16639  idffth  16640  cofull  16641  cofth  16642  ressffth  16645  isnat  16654  natixp  16659  nati  16662  elhomai2  16731  homa1  16734  homahom2  16735  eldmcoa  16762  coapm  16768  catcisolem  16803  catciso  16804  1stfcl  16884  2ndfcl  16885  prfcl  16890  evlfcl  16909  curf1cl  16915  curfcl  16919  hofcl  16946  yonedalem1  16959  yonedalem21  16960  yonedalem22  16965  yonffthlem  16969  yoniso  16972  pospo  17020  efgi  18178  efgi2  18184  gsum2d2lem  18418  dmdprd  18443  dprdval  18448  eldprd  18449  dprd2dlem2  18485  dprd2dlem1  18486  dprd2da  18487  dprd2d2  18489  isunit  18703  subrgdvds  18842  opsrtoslem2  19533  lmrcl  21083  lmff  21153  2ndcctbss  21306  2ndcdisj  21307  hausdiag  21496  hauseqlcld  21497  cnextfun  21915  cnextfvval  21916  cnextfres  21920  tgphaus  21967  utop2nei  22101  utop3cls  22102  ucnima  22132  xmeterval  22284  metustid  22406  metustsym  22407  metustexhalf  22408  elbl4  22415  metuel2  22417  isphtpc  22840  ovolfcl  23281  ovollb2lem  23302  ovolctb  23304  ovolshftlem1  23323  ovolscalem1  23327  ovolicc1  23330  ioombl1lem1  23372  ioorf  23387  dyadf  23405  eldv  23707  dvres2  23721  dvef  23788  eltayl  24159  ulmscl  24178  tglngne  25490  tgelrnln  25570  isperp  25652  brbtwn  25824  iswlk  26562  wlkcpr  26580  wlkcomp  26582  wlkeq  26585  wlklenvclwlk  26607  wlkreslem  26622  clwlkcomp  26731  wlkpwwlkf1ouspgr  26833  wlknwwlksnsur  26844  wlkwwlksur  26851  clwlksfoclwwlk  27050  ex-br  27418  avril1  27449  helloworld  27451  vcex  27561  h2hlm  27965  axhcompl-zf  27983  opeldifid  29538  brabgaf  29546  opabdm  29549  opabrn  29550  fpwrelmap  29636  isarchi  29864  gsummpt2co  29908  qtophaus  30031  prsdm  30088  prsrn  30089  mclsax  31592  brtpid1  31728  brtpid2  31729  brtpid3  31730  brtp  31765  dfso2  31770  dfpo2  31771  fundmpss  31790  opelco3  31802  frrlem5c  31911  scutval  32036  dmscut  32043  scutf  32044  madeval2  32061  pprodss4v  32116  brsset  32121  brtxpsd  32126  sscoid  32145  dffun10  32146  brimg  32169  funpartfun  32175  funpartfv  32177  dfrecs2  32182  dfrdg4  32183  imagesset  32185  fvtransport  32264  brcolinear2  32290  colineardim1  32293  fvray  32373  fvline  32376  eltail  32494  uncf  33518  uncov  33520  unccur  33522  phpreu  33523  poimirlem26  33565  mblfinlem2  33577  areacirclem5  33634  heiborlem3  33742  heiborlem4  33743  heiborlem6  33745  isrngo  33826  rngoablo2  33838  isdivrngo  33879  brvdif2  34167  brvvdif  34168  elecALTV  34171  brresALTV  34173  inxprnres  34201  ssrel3  34208  opelinxp  34251  iss2  34252  brabidga  34268  brabsb2  34466  eqbrrdv2  34467  cmtvalN  34816  cvrval  34874  undmrnresiss  38227  cnvssco  38229  cotrintab  38238  elimaint  38257  coiun1  38261  elintima  38262  briunov2  38291  brtrclfv2  38336  frege77d  38355  dfhe3  38386  dffrege76  38550  frege97  38571  frege98  38572  frege109  38583  frege110  38584  dffrege115  38589  frege131  38605  frege133  38607  rfovcnvf1od  38615  fsovrfovd  38620  fourierdlem42  40684  ovolval2lem  41178  ovolval4lem2  41185  afveu  41554  fnopafvb  41556  tz6.12-afv  41574  tz6.12-1-afv  41575  aovprc  41589  aovrcl  41590  isupwlk  42042  sprsymrelfolem2  42068  sprsymrelf  42070  inclfusubc  42192  funcrngcsetc  42323  funcrngcsetcALT  42324  funcringcsetc  42360
  Copyright terms: Public domain W3C validator