Definition df-br 3930

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 4807). (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 3929	. 2 wff 𝐴𝑅𝐵
5	1, 2	cop 3530	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	wcel 1480	. 2 wff ⟨𝐴, 𝐵⟩ ∈ 𝑅
7	4, 6	wb 104	1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

This definition is referenced by:  breq  3931  breq1  3932  breq2  3933  ssbrd  3971  nfbrd  3973  br0  3976  brne0  3977  brm  3978  brun  3979  brin  3980  brdif  3981  opabss  3992  brabsb  4183  brabga  4186  epelg  4212  pofun  4234  brxp  4570  brab2a  4592  brab2ga  4614  eqbrriv  4634  eqbrrdv  4636  eqbrrdiv  4637  opeliunxp2  4679  opelco2g  4707  opelco  4711  cnvss  4712  elcnv2  4717  opelcnvg  4719  brcnvg  4720  dfdm3  4726  dfrn3  4728  elrng  4730  eldm2g  4735  breldm  4743  dmopab  4750  opelrng  4771  opelrn  4773  elrn  4782  rnopab  4786  brres  4825  brresg  4827  resieq  4829  opelresi  4830  resiexg  4864  iss  4865  dfres2  4871  dfima3  4884  elima3  4888  imai  4895  elimasn  4906  eliniseg  4909  cotr  4920  issref  4921  cnvsym  4922  intasym  4923  asymref  4924  intirr  4925  codir  4927  qfto  4928  poirr2  4931  dmsnm  5004  coiun  5048  co02  5052  coi1  5054  dffun4  5134  dffun4f  5139  funeu2  5149  funopab  5158  funco  5163  funcnvsn  5168  isarep1  5209  fnop  5226  fneu2  5228  brprcneu  5414  dffv3g  5417  tz6.12  5449  nfvres  5454  0fv  5456  funopfv  5461  fnopfvb  5463  fvmptss2  5496  funfvbrb  5533  dff3im  5565  dff4im  5566  f1ompt  5571  idref  5658  foeqcnvco  5691  f1eqcocnv  5692  fliftel  5694  fliftel1  5695  fliftcnv  5696  f1oiso  5727  ovprc  5806  brabvv  5817  1st2ndbr  6082  xporderlem  6128  opeliunxp2f  6135  rbropapd  6139  ottposg  6152  dftpos3  6159  dftpos4  6160  tposoprab  6177  tfrlem7  6214  tfrexlem  6231  ercnv  6450  brdifun  6456  swoord1  6458  swoord2  6459  0er  6463  elecg  6467  iinerm  6501  brecop  6519  idssen  6671  xpcomco  6720  ltdfpr  7314  xrlenlt  7829  aprcl  8408  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  climcau  11116  divides  11495  isstructim  11973  isstructr  11974  lmrcl  12360  lmff  12418  xmeterval  12604  eldvap  12820  dvef  12856