Definition df-br 4045

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 4947). (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 4044	. 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  4046  breq1  4047  breq2  4048  ssbrd  4087  nfbrd  4089  br0  4092  brne0  4093  brm  4094  brun  4095  brin  4096  brdif  4097  opabss  4108  brabsb  4307  brabga  4310  epelg  4337  pofun  4359  brxp  4706  brab2a  4728  brab2ga  4750  eqbrriv  4770  eqbrrdv  4772  eqbrrdiv  4773  opeliunxp2  4818  opelco2g  4846  opelco  4850  cnvss  4851  elcnv2  4856  opelcnvg  4858  brcnvg  4859  dfdm3  4865  dfrn3  4867  elrng  4869  eldm2g  4874  breldm  4882  dmopab  4889  opelrng  4910  opelrn  4912  elrn  4921  rnopab  4925  brres  4965  brresg  4967  resieq  4969  opelresi  4970  resiexg  5004  iss  5005  dfres2  5011  restidsing  5015  dfima3  5025  elima3  5029  imai  5038  elimasn  5049  eliniseg  5052  cotr  5064  issref  5065  cnvsym  5066  intasym  5067  asymref  5068  intirr  5069  codir  5071  qfto  5072  poirr2  5075  dmsnm  5148  coiun  5192  co02  5196  coi1  5198  dffun4  5282  dffun4f  5287  funeu2  5297  funopab  5306  funco  5311  funcnvsn  5319  isarep1  5360  fnop  5379  fneu2  5381  brprcneu  5569  dffv3g  5572  tz6.12  5604  nfvres  5610  0fv  5612  funopfv  5618  fnopfvb  5620  fvmptss2  5654  funfvbrb  5693  dff3im  5725  dff4im  5726  f1ompt  5731  idref  5825  foeqcnvco  5859  f1eqcocnv  5860  fliftel  5862  fliftel1  5863  fliftcnv  5864  f1oiso  5895  ovprc  5980  brabvv  5991  1st2ndbr  6270  xporderlem  6317  opeliunxp2f  6324  rbropapd  6328  ottposg  6341  dftpos3  6348  dftpos4  6349  tposoprab  6366  tfrlem7  6403  tfrexlem  6420  ercnv  6641  brdifun  6647  swoord1  6649  swoord2  6650  0er  6654  elecg  6660  iinerm  6694  brecop  6712  idssen  6868  xpcomco  6921  netap  7366  2omotaplemap  7369  exmidapne  7372  ltdfpr  7619  xrlenlt  8137  aprcl  8719  frecuzrdgtcl  10557  frecuzrdgfunlem  10564  climcau  11658  divides  12100  isstructim  12846  isstructr  12847  imasaddfnlemg  13146  subrgdvds  13997  aprval  14044  lmrcl  14663  lmff  14721  xmeterval  14907  eldvap  15154  dvef  15199