Definition df-br 3792

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 4627). (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 3791	. 2 wff A R B
5	1, 2	cop 3405	. . 3 class <. A , B >.
6	5, 3	wcel 1409	. 2 wff <. A , B >. e. R
7	4, 6	wb 102	1 wff ( A R B <-> <. A , B >. e. R )

This definition is referenced by:  breq  3793  breq1  3794  breq2  3795  ssbrd  3832  nfbrd  3834  brun  3837  brin  3838  brdif  3839  opabss  3848  brabsb  4025  brabga  4028  epelg  4054  pofun  4076  brxp  4402  brab2a  4420  brab2ga  4442  eqbrriv  4462  eqbrrdv  4464  eqbrrdiv  4465  opeliunxp2  4503  opelco2g  4530  opelco  4534  cnvss  4535  elcnv2  4540  opelcnvg  4542  brcnvg  4543  dfdm3  4549  dfrn3  4551  elrng  4553  eldm2g  4558  breldm  4566  dmopab  4573  opelrng  4593  opelrn  4595  elrn  4604  rnopab  4608  brres  4645  brresg  4647  resieq  4649  opelresi  4650  resiexg  4680  iss  4681  dfres2  4685  dfima3  4698  elima3  4702  imai  4708  elimasn  4719  eliniseg  4722  cotr  4733  issref  4734  cnvsym  4735  intasym  4736  asymref  4737  intirr  4738  codir  4740  qfto  4741  poirr2  4744  dmsnm  4813  coiun  4857  co02  4861  coi1  4863  dffun4  4940  dffun4f  4945  funeu2  4954  funopab  4962  funco  4967  funcnvsn  4972  isarep1  5012  fnop  5029  fneu2  5031  brprcneu  5198  dffv3g  5201  tz6.12  5228  nfvres  5233  0fv  5235  funopfv  5240  fnopfvb  5242  fvmptss2  5274  funfvbrb  5307  dff3im  5339  dff4im  5340  f1ompt  5347  idref  5423  foeqcnvco  5457  f1eqcocnv  5458  fliftel  5460  fliftel1  5461  fliftcnv  5462  f1oiso  5492  ovprc  5567  brabvv  5578  1st2ndbr  5837  xporderlem  5879  isprmpt2  5888  ottposg  5900  dftpos3  5907  dftpos4  5908  tposoprab  5925  tfrlem7  5963  tfrexlem  5978  ercnv  6157  brdifun  6163  swoord1  6165  swoord2  6166  0er  6170  elecg  6174  iinerm  6208  brecop  6226  idssen  6287  xpcomco  6330  ltdfpr  6661  xrlenlt  7142  frecuzrdgfn  9361  climcau  10096  divides  10109