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  5622  dffv3g  5625  tz6.12  5657  nfvres  5665  0fv  5667  funopfv  5673  fnopfvb  5675  fvmptss2  5711  funfvbrb  5750  dff3im  5782  dff4im  5783  f1ompt  5788  idref  5886  foeqcnvco  5920  f1eqcocnv  5921  fliftel  5923  fliftel1  5924  fliftcnv  5925  f1oiso  5956  ovprc  6043  brabvv  6056  1st2ndbr  6336  xporderlem  6383  opeliunxp2f  6390  rbropapd  6394  ottposg  6407  dftpos3  6414  dftpos4  6415  tposoprab  6432  tfrlem7  6469  tfrexlem  6486  ercnv  6709  brdifun  6715  swoord1  6717  swoord2  6718  0er  6722  elecg  6728  iinerm  6762  brecop  6780  idssen  6936  xpcomco  6993  netap  7451  2omotaplemap  7454  exmidapne  7457  ltdfpr  7704  xrlenlt  8222  aprcl  8804  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  climcau  11874  divides  12316  isstructim  13062  isstructr  13063  imasaddfnlemg  13363  subrgdvds  14215  aprval  14262  lmrcl  14882  lmff  14939  xmeterval  15125  eldvap  15372  dvef  15417  iswlk  16069  wlkv  16072  wlkcprim  16096  wlklenvclwlk  16119  trlsv  16128  istrl  16129