Definition df-br 4030

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 4930). (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 4029	. 2 wff 𝐴𝑅𝐵
5	1, 2	cop 3621	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	wcel 2164	. 2 wff ⟨𝐴, 𝐵⟩ ∈ 𝑅
7	4, 6	wb 105	1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

This definition is referenced by:  breq  4031  breq1  4032  breq2  4033  ssbrd  4072  nfbrd  4074  br0  4077  brne0  4078  brm  4079  brun  4080  brin  4081  brdif  4082  opabss  4093  brabsb  4291  brabga  4294  epelg  4321  pofun  4343  brxp  4690  brab2a  4712  brab2ga  4734  eqbrriv  4754  eqbrrdv  4756  eqbrrdiv  4757  opeliunxp2  4802  opelco2g  4830  opelco  4834  cnvss  4835  elcnv2  4840  opelcnvg  4842  brcnvg  4843  dfdm3  4849  dfrn3  4851  elrng  4853  eldm2g  4858  breldm  4866  dmopab  4873  opelrng  4894  opelrn  4896  elrn  4905  rnopab  4909  brres  4948  brresg  4950  resieq  4952  opelresi  4953  resiexg  4987  iss  4988  dfres2  4994  restidsing  4998  dfima3  5008  elima3  5012  imai  5021  elimasn  5032  eliniseg  5035  cotr  5047  issref  5048  cnvsym  5049  intasym  5050  asymref  5051  intirr  5052  codir  5054  qfto  5055  poirr2  5058  dmsnm  5131  coiun  5175  co02  5179  coi1  5181  dffun4  5265  dffun4f  5270  funeu2  5280  funopab  5289  funco  5294  funcnvsn  5299  isarep1  5340  fnop  5357  fneu2  5359  brprcneu  5547  dffv3g  5550  tz6.12  5582  nfvres  5588  0fv  5590  funopfv  5596  fnopfvb  5598  fvmptss2  5632  funfvbrb  5671  dff3im  5703  dff4im  5704  f1ompt  5709  idref  5799  foeqcnvco  5833  f1eqcocnv  5834  fliftel  5836  fliftel1  5837  fliftcnv  5838  f1oiso  5869  ovprc  5953  brabvv  5964  1st2ndbr  6237  xporderlem  6284  opeliunxp2f  6291  rbropapd  6295  ottposg  6308  dftpos3  6315  dftpos4  6316  tposoprab  6333  tfrlem7  6370  tfrexlem  6387  ercnv  6608  brdifun  6614  swoord1  6616  swoord2  6617  0er  6621  elecg  6627  iinerm  6661  brecop  6679  idssen  6831  xpcomco  6880  netap  7314  2omotaplemap  7317  exmidapne  7320  ltdfpr  7566  xrlenlt  8084  aprcl  8665  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  climcau  11490  divides  11932  isstructim  12632  isstructr  12633  imasaddfnlemg  12897  subrgdvds  13731  aprval  13778  lmrcl  14359  lmff  14417  xmeterval  14603  eldvap  14836  dvef  14873