Definition df-br 3823

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 4671). (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 3822	. 2 wff A R B
5	1, 2	cop 3434	. . 3 class <. A , B >.
6	5, 3	wcel 1436	. 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  3824  breq1  3825  breq2  3826  ssbrd  3863  nfbrd  3865  brun  3868  brin  3869  brdif  3870  opabss  3879  brabsb  4064  brabga  4067  epelg  4093  pofun  4115  brxp  4443  brab2a  4461  brab2ga  4483  eqbrriv  4503  eqbrrdv  4505  eqbrrdiv  4506  opeliunxp2  4546  opelco2g  4574  opelco  4578  cnvss  4579  elcnv2  4584  opelcnvg  4586  brcnvg  4587  dfdm3  4593  dfrn3  4595  elrng  4597  eldm2g  4602  breldm  4610  dmopab  4617  opelrng  4637  opelrn  4639  elrn  4648  rnopab  4652  brres  4689  brresg  4691  resieq  4693  opelresi  4694  resiexg  4726  iss  4727  dfres2  4733  dfima3  4746  elima3  4750  imai  4757  elimasn  4768  eliniseg  4771  cotr  4782  issref  4783  cnvsym  4784  intasym  4785  asymref  4786  intirr  4787  codir  4789  qfto  4790  poirr2  4793  dmsnm  4864  coiun  4908  co02  4912  coi1  4914  dffun4  4994  dffun4f  4999  funeu2  5008  funopab  5016  funco  5021  funcnvsn  5026  isarep1  5067  fnop  5084  fneu2  5086  brprcneu  5263  dffv3g  5266  tz6.12  5297  nfvres  5302  0fv  5304  funopfv  5309  fnopfvb  5311  fvmptss2  5344  funfvbrb  5377  dff3im  5409  dff4im  5410  f1ompt  5415  idref  5499  foeqcnvco  5532  f1eqcocnv  5533  fliftel  5535  fliftel1  5536  fliftcnv  5537  f1oiso  5568  ovprc  5643  brabvv  5654  1st2ndbr  5913  xporderlem  5955  isprmpt2  5964  ottposg  5976  dftpos3  5983  dftpos4  5984  tposoprab  6001  tfrlem7  6038  tfrexlem  6055  ercnv  6267  brdifun  6273  swoord1  6275  swoord2  6276  0er  6280  elecg  6284  iinerm  6318  brecop  6336  idssen  6448  xpcomco  6496  ltdfpr  7012  xrlenlt  7498  frecuzrdgtcl  9750  frecuzrdgfunlem  9757  climcau  10631  divides  10704