Definition df-br 4035

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 4935). (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 4034	. 2 wff A R B
5	1, 2	cop 3626	. . 3 class <. A , B >.
6	5, 3	wcel 2167	. 2 wff <. A , B >. e. R
7	4, 6	wb 105	1 wff ( A R B <-> <. A , B >. e. R )

This definition is referenced by:  breq  4036  breq1  4037  breq2  4038  ssbrd  4077  nfbrd  4079  br0  4082  brne0  4083  brm  4084  brun  4085  brin  4086  brdif  4087  opabss  4098  brabsb  4296  brabga  4299  epelg  4326  pofun  4348  brxp  4695  brab2a  4717  brab2ga  4739  eqbrriv  4759  eqbrrdv  4761  eqbrrdiv  4762  opeliunxp2  4807  opelco2g  4835  opelco  4839  cnvss  4840  elcnv2  4845  opelcnvg  4847  brcnvg  4848  dfdm3  4854  dfrn3  4856  elrng  4858  eldm2g  4863  breldm  4871  dmopab  4878  opelrng  4899  opelrn  4901  elrn  4910  rnopab  4914  brres  4953  brresg  4955  resieq  4957  opelresi  4958  resiexg  4992  iss  4993  dfres2  4999  restidsing  5003  dfima3  5013  elima3  5017  imai  5026  elimasn  5037  eliniseg  5040  cotr  5052  issref  5053  cnvsym  5054  intasym  5055  asymref  5056  intirr  5057  codir  5059  qfto  5060  poirr2  5063  dmsnm  5136  coiun  5180  co02  5184  coi1  5186  dffun4  5270  dffun4f  5275  funeu2  5285  funopab  5294  funco  5299  funcnvsn  5304  isarep1  5345  fnop  5364  fneu2  5366  brprcneu  5554  dffv3g  5557  tz6.12  5589  nfvres  5595  0fv  5597  funopfv  5603  fnopfvb  5605  fvmptss2  5639  funfvbrb  5678  dff3im  5710  dff4im  5711  f1ompt  5716  idref  5806  foeqcnvco  5840  f1eqcocnv  5841  fliftel  5843  fliftel1  5844  fliftcnv  5845  f1oiso  5876  ovprc  5961  brabvv  5972  1st2ndbr  6251  xporderlem  6298  opeliunxp2f  6305  rbropapd  6309  ottposg  6322  dftpos3  6329  dftpos4  6330  tposoprab  6347  tfrlem7  6384  tfrexlem  6401  ercnv  6622  brdifun  6628  swoord1  6630  swoord2  6631  0er  6635  elecg  6641  iinerm  6675  brecop  6693  idssen  6845  xpcomco  6894  netap  7337  2omotaplemap  7340  exmidapne  7343  ltdfpr  7590  xrlenlt  8108  aprcl  8690  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  climcau  11529  divides  11971  isstructim  12717  isstructr  12718  imasaddfnlemg  13016  subrgdvds  13867  aprval  13914  lmrcl  14511  lmff  14569  xmeterval  14755  eldvap  15002  dvef  15047