Definition df-br 3807

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 R is a proper class (see for example iprc 4649). (Contributed by NM, 31-Dec-1993.)

Assertion

Ref	Expression
df-br	|- ( A R B <-> <. A , B >. e. R )

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 R
4	1, 2, 3	wbr 3806	. 2 wff A R B
5	1, 2	cop 3420	. . 3 class <. A , B >.
6	5, 3	wcel 1434	. 2 wff <. A , B >. e. R
7	4, 6	wb 103	1 wff ( A R B <-> <. A , B >. e. R )

This definition is referenced by:  breq  3808  breq1  3809  breq2  3810  ssbrd  3847  nfbrd  3849  brun  3852  brin  3853  brdif  3854  opabss  3863  brabsb  4045  brabga  4048  epelg  4074  pofun  4096  brxp  4422  brab2a  4440  brab2ga  4462  eqbrriv  4482  eqbrrdv  4484  eqbrrdiv  4485  opeliunxp2  4525  opelco2g  4552  opelco  4556  cnvss  4557  elcnv2  4562  opelcnvg  4564  brcnvg  4565  dfdm3  4571  dfrn3  4573  elrng  4575  eldm2g  4580  breldm  4588  dmopab  4595  opelrng  4615  opelrn  4617  elrn  4626  rnopab  4630  brres  4667  brresg  4669  resieq  4671  opelresi  4672  resiexg  4704  iss  4705  dfres2  4709  dfima3  4722  elima3  4726  imai  4732  elimasn  4743  eliniseg  4746  cotr  4757  issref  4758  cnvsym  4759  intasym  4760  asymref  4761  intirr  4762  codir  4764  qfto  4765  poirr2  4768  dmsnm  4837  coiun  4881  co02  4885  coi1  4887  dffun4  4964  dffun4f  4969  funeu2  4978  funopab  4986  funco  4991  funcnvsn  4996  isarep1  5037  fnop  5054  fneu2  5056  brprcneu  5224  dffv3g  5227  tz6.12  5255  nfvres  5260  0fv  5262  funopfv  5267  fnopfvb  5269  fvmptss2  5301  funfvbrb  5334  dff3im  5366  dff4im  5367  f1ompt  5374  idref  5450  foeqcnvco  5483  f1eqcocnv  5484  fliftel  5486  fliftel1  5487  fliftcnv  5488  f1oiso  5518  ovprc  5593  brabvv  5604  1st2ndbr  5863  xporderlem  5905  isprmpt2  5914  ottposg  5926  dftpos3  5933  dftpos4  5934  tposoprab  5951  tfrlem7  5988  tfrexlem  6005  ercnv  6216  brdifun  6222  swoord1  6224  swoord2  6225  0er  6229  elecg  6233  iinerm  6267  brecop  6285  idssen  6347  xpcomco  6393  ltdfpr  6835  xrlenlt  7321  frecuzrdgtcl  9571  frecuzrdgfunlem  9578  climcau  10410  divides  10430