Definition df-br 4004

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 4895). (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 4003	. 2 wff 𝐴𝑅𝐵
5	1, 2	cop 3595	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	wcel 2148	. 2 wff ⟨𝐴, 𝐵⟩ ∈ 𝑅
7	4, 6	wb 105	1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

This definition is referenced by:  breq  4005  breq1  4006  breq2  4007  ssbrd  4046  nfbrd  4048  br0  4051  brne0  4052  brm  4053  brun  4054  brin  4055  brdif  4056  opabss  4067  brabsb  4261  brabga  4264  epelg  4290  pofun  4312  brxp  4657  brab2a  4679  brab2ga  4701  eqbrriv  4721  eqbrrdv  4723  eqbrrdiv  4724  opeliunxp2  4767  opelco2g  4795  opelco  4799  cnvss  4800  elcnv2  4805  opelcnvg  4807  brcnvg  4808  dfdm3  4814  dfrn3  4816  elrng  4818  eldm2g  4823  breldm  4831  dmopab  4838  opelrng  4859  opelrn  4861  elrn  4870  rnopab  4874  brres  4913  brresg  4915  resieq  4917  opelresi  4918  resiexg  4952  iss  4953  dfres2  4959  restidsing  4963  dfima3  4973  elima3  4977  imai  4984  elimasn  4995  eliniseg  4998  cotr  5010  issref  5011  cnvsym  5012  intasym  5013  asymref  5014  intirr  5015  codir  5017  qfto  5018  poirr2  5021  dmsnm  5094  coiun  5138  co02  5142  coi1  5144  dffun4  5227  dffun4f  5232  funeu2  5242  funopab  5251  funco  5256  funcnvsn  5261  isarep1  5302  fnop  5319  fneu2  5321  brprcneu  5508  dffv3g  5511  tz6.12  5543  nfvres  5548  0fv  5550  funopfv  5555  fnopfvb  5557  fvmptss2  5591  funfvbrb  5629  dff3im  5661  dff4im  5662  f1ompt  5667  idref  5757  foeqcnvco  5790  f1eqcocnv  5791  fliftel  5793  fliftel1  5794  fliftcnv  5795  f1oiso  5826  ovprc  5909  brabvv  5920  1st2ndbr  6184  xporderlem  6231  opeliunxp2f  6238  rbropapd  6242  ottposg  6255  dftpos3  6262  dftpos4  6263  tposoprab  6280  tfrlem7  6317  tfrexlem  6334  ercnv  6555  brdifun  6561  swoord1  6563  swoord2  6564  0er  6568  elecg  6572  iinerm  6606  brecop  6624  idssen  6776  xpcomco  6825  netap  7252  2omotaplemap  7255  exmidapne  7258  ltdfpr  7504  xrlenlt  8021  aprcl  8602  frecuzrdgtcl  10411  frecuzrdgfunlem  10418  climcau  11354  divides  11795  isstructim  12475  isstructr  12476  imasaddfnlemg  12734  subrgdvds  13354  aprval  13370  lmrcl  13661  lmff  13719  xmeterval  13905  eldvap  14121  dvef  14158