Definition df-br 4084

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 4993). (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 4083	. 2 wff 𝐴𝑅𝐵
5	1, 2	cop 3669	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	wcel 2200	. 2 wff ⟨𝐴, 𝐵⟩ ∈ 𝑅
7	4, 6	wb 105	1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

This definition is referenced by:  breq  4085  breq1  4086  breq2  4087  ssbrd  4126  nfbrd  4129  br0  4132  brne0  4133  brm  4134  brun  4135  brin  4136  brdif  4137  opabss  4148  brabsb  4349  brabga  4352  epelg  4381  pofun  4403  brxp  4750  brab2a  4772  brab2ga  4794  eqbrriv  4814  eqbrrdv  4816  eqbrrdiv  4817  opeliunxp2  4862  opelco2g  4890  opelco  4894  cnvss  4895  elcnv2  4900  opelcnvg  4902  brcnvg  4903  dfdm3  4909  dfrn3  4911  elrng  4913  eldm2g  4919  breldm  4927  dmopab  4934  opelrng  4956  opelrn  4958  elrn  4967  rnopab  4971  brres  5011  brresg  5013  resieq  5015  opelresi  5016  resiexg  5050  iss  5051  dfres2  5057  restidsing  5061  dfima3  5071  elima3  5075  imai  5084  elimasn  5095  eliniseg  5098  cotr  5110  issref  5111  cnvsym  5112  intasym  5113  asymref  5114  intirr  5115  codir  5117  qfto  5118  poirr2  5121  dmsnm  5194  coiun  5238  co02  5242  coi1  5244  dffun4  5329  dffun4f  5334  funeu2  5344  funopab  5353  funco  5358  funcnvsn  5366  isarep1  5407  fnop  5426  fneu2  5428  brprcneu  5620  dffv3g  5623  tz6.12  5655  nfvres  5663  0fv  5665  funopfv  5671  fnopfvb  5673  fvmptss2  5709  funfvbrb  5748  dff3im  5780  dff4im  5781  f1ompt  5786  idref  5880  foeqcnvco  5914  f1eqcocnv  5915  fliftel  5917  fliftel1  5918  fliftcnv  5919  f1oiso  5950  ovprc  6037  brabvv  6050  1st2ndbr  6330  xporderlem  6377  opeliunxp2f  6384  rbropapd  6388  ottposg  6401  dftpos3  6408  dftpos4  6409  tposoprab  6426  tfrlem7  6463  tfrexlem  6480  ercnv  6701  brdifun  6707  swoord1  6709  swoord2  6710  0er  6714  elecg  6720  iinerm  6754  brecop  6772  idssen  6928  xpcomco  6985  netap  7440  2omotaplemap  7443  exmidapne  7446  ltdfpr  7693  xrlenlt  8211  aprcl  8793  frecuzrdgtcl  10634  frecuzrdgfunlem  10641  climcau  11858  divides  12300  isstructim  13046  isstructr  13047  imasaddfnlemg  13347  subrgdvds  14199  aprval  14246  lmrcl  14866  lmff  14923  xmeterval  15109  eldvap  15356  dvef  15401  iswlk  16036  wlkv  16038  wlkcprim  16061  wlklenvclwlk  16084