Definition df-br 3982

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 4871). (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 3981	. 2 wff 𝐴𝑅𝐵
5	1, 2	cop 3578	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	wcel 2136	. 2 wff ⟨𝐴, 𝐵⟩ ∈ 𝑅
7	4, 6	wb 104	1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

This definition is referenced by:  breq  3983  breq1  3984  breq2  3985  ssbrd  4024  nfbrd  4026  br0  4029  brne0  4030  brm  4031  brun  4032  brin  4033  brdif  4034  opabss  4045  brabsb  4238  brabga  4241  epelg  4267  pofun  4289  brxp  4634  brab2a  4656  brab2ga  4678  eqbrriv  4698  eqbrrdv  4700  eqbrrdiv  4701  opeliunxp2  4743  opelco2g  4771  opelco  4775  cnvss  4776  elcnv2  4781  opelcnvg  4783  brcnvg  4784  dfdm3  4790  dfrn3  4792  elrng  4794  eldm2g  4799  breldm  4807  dmopab  4814  opelrng  4835  opelrn  4837  elrn  4846  rnopab  4850  brres  4889  brresg  4891  resieq  4893  opelresi  4894  resiexg  4928  iss  4929  dfres2  4935  dfima3  4948  elima3  4952  imai  4959  elimasn  4970  eliniseg  4973  cotr  4984  issref  4985  cnvsym  4986  intasym  4987  asymref  4988  intirr  4989  codir  4991  qfto  4992  poirr2  4995  dmsnm  5068  coiun  5112  co02  5116  coi1  5118  dffun4  5198  dffun4f  5203  funeu2  5213  funopab  5222  funco  5227  funcnvsn  5232  isarep1  5273  fnop  5290  fneu2  5292  brprcneu  5478  dffv3g  5481  tz6.12  5513  nfvres  5518  0fv  5520  funopfv  5525  fnopfvb  5527  fvmptss2  5560  funfvbrb  5597  dff3im  5629  dff4im  5630  f1ompt  5635  idref  5724  foeqcnvco  5757  f1eqcocnv  5758  fliftel  5760  fliftel1  5761  fliftcnv  5762  f1oiso  5793  ovprc  5873  brabvv  5884  1st2ndbr  6149  xporderlem  6195  opeliunxp2f  6202  rbropapd  6206  ottposg  6219  dftpos3  6226  dftpos4  6227  tposoprab  6244  tfrlem7  6281  tfrexlem  6298  ercnv  6518  brdifun  6524  swoord1  6526  swoord2  6527  0er  6531  elecg  6535  iinerm  6569  brecop  6587  idssen  6739  xpcomco  6788  ltdfpr  7443  xrlenlt  7959  aprcl  8540  frecuzrdgtcl  10343  frecuzrdgfunlem  10350  climcau  11284  divides  11725  isstructim  12404  isstructr  12405  lmrcl  12791  lmff  12849  xmeterval  13035  eldvap  13251  dvef  13288