Definition df-br 4046

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 4948). (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 4045	. 2 wff 𝐴𝑅𝐵
5	1, 2	cop 3636	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	wcel 2176	. 2 wff ⟨𝐴, 𝐵⟩ ∈ 𝑅
7	4, 6	wb 105	1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

This definition is referenced by:  breq  4047  breq1  4048  breq2  4049  ssbrd  4088  nfbrd  4090  br0  4093  brne0  4094  brm  4095  brun  4096  brin  4097  brdif  4098  opabss  4109  brabsb  4308  brabga  4311  epelg  4338  pofun  4360  brxp  4707  brab2a  4729  brab2ga  4751  eqbrriv  4771  eqbrrdv  4773  eqbrrdiv  4774  opeliunxp2  4819  opelco2g  4847  opelco  4851  cnvss  4852  elcnv2  4857  opelcnvg  4859  brcnvg  4860  dfdm3  4866  dfrn3  4868  elrng  4870  eldm2g  4875  breldm  4883  dmopab  4890  opelrng  4911  opelrn  4913  elrn  4922  rnopab  4926  brres  4966  brresg  4968  resieq  4970  opelresi  4971  resiexg  5005  iss  5006  dfres2  5012  restidsing  5016  dfima3  5026  elima3  5030  imai  5039  elimasn  5050  eliniseg  5053  cotr  5065  issref  5066  cnvsym  5067  intasym  5068  asymref  5069  intirr  5070  codir  5072  qfto  5073  poirr2  5076  dmsnm  5149  coiun  5193  co02  5197  coi1  5199  dffun4  5283  dffun4f  5288  funeu2  5298  funopab  5307  funco  5312  funcnvsn  5320  isarep1  5361  fnop  5380  fneu2  5382  brprcneu  5571  dffv3g  5574  tz6.12  5606  nfvres  5612  0fv  5614  funopfv  5620  fnopfvb  5622  fvmptss2  5656  funfvbrb  5695  dff3im  5727  dff4im  5728  f1ompt  5733  idref  5827  foeqcnvco  5861  f1eqcocnv  5862  fliftel  5864  fliftel1  5865  fliftcnv  5866  f1oiso  5897  ovprc  5982  brabvv  5993  1st2ndbr  6272  xporderlem  6319  opeliunxp2f  6326  rbropapd  6330  ottposg  6343  dftpos3  6350  dftpos4  6351  tposoprab  6368  tfrlem7  6405  tfrexlem  6422  ercnv  6643  brdifun  6649  swoord1  6651  swoord2  6652  0er  6656  elecg  6662  iinerm  6696  brecop  6714  idssen  6870  xpcomco  6923  netap  7368  2omotaplemap  7371  exmidapne  7374  ltdfpr  7621  xrlenlt  8139  aprcl  8721  frecuzrdgtcl  10559  frecuzrdgfunlem  10566  climcau  11691  divides  12133  isstructim  12879  isstructr  12880  imasaddfnlemg  13179  subrgdvds  14030  aprval  14077  lmrcl  14696  lmff  14754  xmeterval  14940  eldvap  15187  dvef  15232