Definition df-br 3966

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. 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 4853). (Contributed by NM, 31-Dec-1993.)

Assertion

Ref	Expression
df-br	⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

Detailed syntax breakdown of Definition df-br

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cR	. . 3 class 𝑅
4	1, 2, 3	wbr 3965	. 2 wff 𝐴𝑅𝐵
5	1, 2	cop 3563	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	wcel 2128	. 2 wff ⟨𝐴, 𝐵⟩ ∈ 𝑅
7	4, 6	wb 104	1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

This definition is referenced by:  breq  3967  breq1  3968  breq2  3969  ssbrd  4007  nfbrd  4009  br0  4012  brne0  4013  brm  4014  brun  4015  brin  4016  brdif  4017  opabss  4028  brabsb  4221  brabga  4224  epelg  4250  pofun  4272  brxp  4616  brab2a  4638  brab2ga  4660  eqbrriv  4680  eqbrrdv  4682  eqbrrdiv  4683  opeliunxp2  4725  opelco2g  4753  opelco  4757  cnvss  4758  elcnv2  4763  opelcnvg  4765  brcnvg  4766  dfdm3  4772  dfrn3  4774  elrng  4776  eldm2g  4781  breldm  4789  dmopab  4796  opelrng  4817  opelrn  4819  elrn  4828  rnopab  4832  brres  4871  brresg  4873  resieq  4875  opelresi  4876  resiexg  4910  iss  4911  dfres2  4917  dfima3  4930  elima3  4934  imai  4941  elimasn  4952  eliniseg  4955  cotr  4966  issref  4967  cnvsym  4968  intasym  4969  asymref  4970  intirr  4971  codir  4973  qfto  4974  poirr2  4977  dmsnm  5050  coiun  5094  co02  5098  coi1  5100  dffun4  5180  dffun4f  5185  funeu2  5195  funopab  5204  funco  5209  funcnvsn  5214  isarep1  5255  fnop  5272  fneu2  5274  brprcneu  5460  dffv3g  5463  tz6.12  5495  nfvres  5500  0fv  5502  funopfv  5507  fnopfvb  5509  fvmptss2  5542  funfvbrb  5579  dff3im  5611  dff4im  5612  f1ompt  5617  idref  5704  foeqcnvco  5737  f1eqcocnv  5738  fliftel  5740  fliftel1  5741  fliftcnv  5742  f1oiso  5773  ovprc  5853  brabvv  5864  1st2ndbr  6129  xporderlem  6175  opeliunxp2f  6182  rbropapd  6186  ottposg  6199  dftpos3  6206  dftpos4  6207  tposoprab  6224  tfrlem7  6261  tfrexlem  6278  ercnv  6498  brdifun  6504  swoord1  6506  swoord2  6507  0er  6511  elecg  6515  iinerm  6549  brecop  6567  idssen  6719  xpcomco  6768  ltdfpr  7420  xrlenlt  7936  aprcl  8515  frecuzrdgtcl  10304  frecuzrdgfunlem  10311  climcau  11237  divides  11678  isstructim  12175  isstructr  12176  lmrcl  12562  lmff  12620  xmeterval  12806  eldvap  13022  dvef  13059