Definition df-br 3786

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 4618). (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 3785	. 2 wff A R B
5	1, 2	cop 3401	. . 3 class <. A , B >.
6	5, 3	wcel 1433	. 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  3787  breq1  3788  breq2  3789  ssbrd  3826  nfbrd  3828  brun  3831  brin  3832  brdif  3833  opabss  3842  brabsb  4016  brabga  4019  epelg  4045  pofun  4067  brxp  4393  brab2a  4411  brab2ga  4433  eqbrriv  4453  eqbrrdv  4455  eqbrrdiv  4456  opeliunxp2  4494  opelco2g  4521  opelco  4525  cnvss  4526  elcnv2  4531  opelcnvg  4533  brcnvg  4534  dfdm3  4540  dfrn3  4542  elrng  4544  eldm2g  4549  breldm  4557  dmopab  4564  opelrng  4584  opelrn  4586  elrn  4595  rnopab  4599  brres  4636  brresg  4638  resieq  4640  opelresi  4641  resiexg  4673  iss  4674  dfres2  4678  dfima3  4691  elima3  4695  imai  4701  elimasn  4712  eliniseg  4715  cotr  4726  issref  4727  cnvsym  4728  intasym  4729  asymref  4730  intirr  4731  codir  4733  qfto  4734  poirr2  4737  dmsnm  4806  coiun  4850  co02  4854  coi1  4856  dffun4  4933  dffun4f  4938  funeu2  4947  funopab  4955  funco  4960  funcnvsn  4965  isarep1  5005  fnop  5022  fneu2  5024  brprcneu  5191  dffv3g  5194  tz6.12  5222  nfvres  5227  0fv  5229  funopfv  5234  fnopfvb  5236  fvmptss2  5268  funfvbrb  5301  dff3im  5333  dff4im  5334  f1ompt  5341  idref  5417  foeqcnvco  5450  f1eqcocnv  5451  fliftel  5453  fliftel1  5454  fliftcnv  5455  f1oiso  5485  ovprc  5560  brabvv  5571  1st2ndbr  5830  xporderlem  5872  isprmpt2  5881  ottposg  5893  dftpos3  5900  dftpos4  5901  tposoprab  5918  tfrlem7  5956  tfrexlem  5971  ercnv  6150  brdifun  6156  swoord1  6158  swoord2  6159  0er  6163  elecg  6167  iinerm  6201  brecop  6219  idssen  6280  xpcomco  6323  ltdfpr  6696  xrlenlt  7177  frecuzrdgfn  9414  climcau  10184  divides  10197