Definition df-br 3762

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

This definition is referenced by:  breq  3763  breq1  3764  breq2  3765  ssbrd  3802  nfbrd  3804  brun  3807  brin  3808  brdif  3809  opabss  3818  brabsb  3995  brabga  3998  epelg  4024  pofun  4046  brxp  4353  brab2a  4371  brab2ga  4393  eqbrriv  4413  eqbrrdv  4415  eqbrrdiv  4416  opeliunxp2  4454  opelco2g  4481  opelco  4485  cnvss  4486  elcnv2  4491  opelcnvg  4493  brcnvg  4494  dfdm3  4500  dfrn3  4502  elrng  4504  eldm2g  4509  breldm  4517  dmopab  4524  opelrng  4544  opelrn  4546  elrn  4555  rnopab  4559  brres  4596  brresg  4598  resieq  4600  opelresi  4601  resiexg  4631  iss  4632  dfres2  4636  dfima3  4649  elima3  4653  imai  4659  elimasn  4670  eliniseg  4673  cotr  4684  issref  4685  cnvsym  4686  intasym  4687  asymref  4688  intirr  4689  codir  4691  qfto  4692  poirr2  4695  dmsnm  4764  coiun  4808  co02  4812  coi1  4814  dffun4  4891  dffun4f  4896  funeu2  4905  funopab  4913  funco  4918  funcnvsn  4923  isarep1  4963  fnop  4980  fneu2  4982  brprcneu  5149  dffv3g  5152  tz6.12  5179  nfvres  5184  0fv  5186  funopfv  5191  fnopfvb  5193  fvmptss2  5225  funfvbrb  5258  dff3im  5290  dff4im  5291  f1ompt  5298  idref  5374  foeqcnvco  5408  f1eqcocnv  5409  fliftel  5411  fliftel1  5412  fliftcnv  5413  f1oiso  5443  ovprc  5518  brabvv  5529  1st2ndbr  5788  xporderlem  5830  isprmpt2  5836  ottposg  5848  dftpos3  5855  dftpos4  5856  tposoprab  5873  tfrlem7  5911  tfrexlem  5926  ercnv  6105  brdifun  6111  swoord1  6113  swoord2  6114  0er  6118  elecg  6122  iinerm  6156  brecop  6174  idssen  6235  xpcomco  6278  ltdfpr  6576  xrlenlt  7055  frecuzrdgfn  9067  climcau  9734