Definition df-br 3735

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 A and/or B 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 4523). (Contributed by NM, 31-Dec-1993.)

Assertion

Ref	Expression
df-br	⊢ (A𝑅B ↔ ⟨A, B⟩ ∈ 𝑅)

Detailed syntax breakdown of Definition df-br

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cR	. . 3 class 𝑅
4	1, 2, 3	wbr 3734	. 2 wff A𝑅B
5	1, 2	cop 3349	. . 3 class ⟨A, B⟩
6	5, 3	wcel 1370	. 2 wff ⟨A, B⟩ ∈ 𝑅
7	4, 6	wb 98	1 wff (A𝑅B ↔ ⟨A, B⟩ ∈ 𝑅)

This definition is referenced by:  breq  3736  breq1  3737  breq2  3738  ssbrd  3775  nfbrd  3777  brun  3780  brin  3781  brdif  3782  opabss  3791  brabsb  3968  brabga  3971  epelg  3997  pofun  4019  brxp  4298  brab2a  4316  brab2ga  4338  eqbrriv  4358  eqbrrdv  4360  eqbrrdiv  4361  opeliunxp2  4399  opelco2g  4426  opelco  4430  cnvss  4431  elcnv2  4436  opelcnvg  4438  brcnvg  4439  dfdm3  4445  dfrn3  4447  elrng  4449  eldm2g  4454  breldm  4462  dmopab  4469  opelrng  4489  opelrn  4491  elrn  4500  rnopab  4504  brres  4541  brresg  4543  resieq  4545  opelresi  4546  resiexg  4576  iss  4577  dfres2  4581  dfima3  4594  elima3  4598  imai  4604  elimasn  4615  eliniseg  4618  cotr  4629  issref  4630  cnvsym  4631  intasym  4632  asymref  4633  intirr  4634  codir  4636  qfto  4637  poirr2  4640  dmsnm  4709  coiun  4753  co02  4757  coi1  4759  dffun4  4836  dffun4f  4840  funeu2  4849  funopab  4857  funco  4862  funcnvsn  4867  isarep1  4907  fnop  4924  fneu2  4926  brprcneu  5092  dffv3g  5095  tz6.12  5122  nfvres  5127  0fv  5129  funopfv  5134  fnopfvb  5136  fvmptss2  5168  funfvbrb  5201  dff3im  5233  dff4im  5234  f1ompt  5241  idref  5317  foeqcnvco  5351  f1eqcocnv  5352  fliftel  5354  fliftel1  5355  fliftcnv  5356  f1oiso  5386  ovprc  5459  brabvv  5470  1st2ndbr  5729  xporderlem  5770  isprmpt2  5776  ottposg  5788  dftpos3  5795  dftpos4  5796  tposoprab  5813  tfrlem7  5851  tfrexlem  5866  ercnv  6034  brdifun  6040  swoord1  6042  swoord2  6043  0er  6047  elecg  6051  iinerm  6085  brecop  6103  ltdfpr  6354  xrlenlt  6679