Definition df-br 3765

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 4600). (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 3764	. 2 wff 𝐴𝑅𝐵
5	1, 2	cop 3378	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	wcel 1393	. 2 wff ⟨𝐴, 𝐵⟩ ∈ 𝑅
7	4, 6	wb 98	1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

This definition is referenced by:  breq  3766  breq1  3767  breq2  3768  ssbrd  3805  nfbrd  3807  brun  3810  brin  3811  brdif  3812  opabss  3821  brabsb  3998  brabga  4001  epelg  4027  pofun  4049  brxp  4375  brab2a  4393  brab2ga  4415  eqbrriv  4435  eqbrrdv  4437  eqbrrdiv  4438  opeliunxp2  4476  opelco2g  4503  opelco  4507  cnvss  4508  elcnv2  4513  opelcnvg  4515  brcnvg  4516  dfdm3  4522  dfrn3  4524  elrng  4526  eldm2g  4531  breldm  4539  dmopab  4546  opelrng  4566  opelrn  4568  elrn  4577  rnopab  4581  brres  4618  brresg  4620  resieq  4622  opelresi  4623  resiexg  4653  iss  4654  dfres2  4658  dfima3  4671  elima3  4675  imai  4681  elimasn  4692  eliniseg  4695  cotr  4706  issref  4707  cnvsym  4708  intasym  4709  asymref  4710  intirr  4711  codir  4713  qfto  4714  poirr2  4717  dmsnm  4786  coiun  4830  co02  4834  coi1  4836  dffun4  4913  dffun4f  4918  funeu2  4927  funopab  4935  funco  4940  funcnvsn  4945  isarep1  4985  fnop  5002  fneu2  5004  brprcneu  5171  dffv3g  5174  tz6.12  5201  nfvres  5206  0fv  5208  funopfv  5213  fnopfvb  5215  fvmptss2  5247  funfvbrb  5280  dff3im  5312  dff4im  5313  f1ompt  5320  idref  5396  foeqcnvco  5430  f1eqcocnv  5431  fliftel  5433  fliftel1  5434  fliftcnv  5435  f1oiso  5465  ovprc  5540  brabvv  5551  1st2ndbr  5810  xporderlem  5852  isprmpt2  5858  ottposg  5870  dftpos3  5877  dftpos4  5878  tposoprab  5895  tfrlem7  5933  tfrexlem  5948  ercnv  6127  brdifun  6133  swoord1  6135  swoord2  6136  0er  6140  elecg  6144  iinerm  6178  brecop  6196  idssen  6257  xpcomco  6300  ltdfpr  6604  xrlenlt  7084  frecuzrdgfn  9198  climcau  9866