Definition df-br 3756

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 4543). (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 3755	. 2 wff A𝑅B
5	1, 2	cop 3370	. . 3 class ⟨A, B⟩
6	5, 3	wcel 1390	. 2 wff ⟨A, B⟩ ∈ 𝑅
7	4, 6	wb 98	1 wff (A𝑅B ↔ ⟨A, B⟩ ∈ 𝑅)

This definition is referenced by:  breq  3757  breq1  3758  breq2  3759  ssbrd  3796  nfbrd  3798  brun  3801  brin  3802  brdif  3803  opabss  3812  brabsb  3989  brabga  3992  epelg  4018  pofun  4040  brxp  4318  brab2a  4336  brab2ga  4358  eqbrriv  4378  eqbrrdv  4380  eqbrrdiv  4381  opeliunxp2  4419  opelco2g  4446  opelco  4450  cnvss  4451  elcnv2  4456  opelcnvg  4458  brcnvg  4459  dfdm3  4465  dfrn3  4467  elrng  4469  eldm2g  4474  breldm  4482  dmopab  4489  opelrng  4509  opelrn  4511  elrn  4520  rnopab  4524  brres  4561  brresg  4563  resieq  4565  opelresi  4566  resiexg  4596  iss  4597  dfres2  4601  dfima3  4614  elima3  4618  imai  4624  elimasn  4635  eliniseg  4638  cotr  4649  issref  4650  cnvsym  4651  intasym  4652  asymref  4653  intirr  4654  codir  4656  qfto  4657  poirr2  4660  dmsnm  4729  coiun  4773  co02  4777  coi1  4779  dffun4  4856  dffun4f  4861  funeu2  4870  funopab  4878  funco  4883  funcnvsn  4888  isarep1  4928  fnop  4945  fneu2  4947  brprcneu  5114  dffv3g  5117  tz6.12  5144  nfvres  5149  0fv  5151  funopfv  5156  fnopfvb  5158  fvmptss2  5190  funfvbrb  5223  dff3im  5255  dff4im  5256  f1ompt  5263  idref  5339  foeqcnvco  5373  f1eqcocnv  5374  fliftel  5376  fliftel1  5377  fliftcnv  5378  f1oiso  5408  ovprc  5482  brabvv  5493  1st2ndbr  5752  xporderlem  5793  isprmpt2  5799  ottposg  5811  dftpos3  5818  dftpos4  5819  tposoprab  5836  tfrlem7  5874  tfrexlem  5889  ercnv  6063  brdifun  6069  swoord1  6071  swoord2  6072  0er  6076  elecg  6080  iinerm  6114  brecop  6132  idssen  6193  xpcomco  6236  ltdfpr  6488  xrlenlt  6841  frecuzrdgfn  8839