Definition df-br 4019

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 4913). (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 4018	. 2 wff A R B
5	1, 2	cop 3610	. . 3 class <. A , B >.
6	5, 3	wcel 2160	. 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  4020  breq1  4021  breq2  4022  ssbrd  4061  nfbrd  4063  br0  4066  brne0  4067  brm  4068  brun  4069  brin  4070  brdif  4071  opabss  4082  brabsb  4279  brabga  4282  epelg  4308  pofun  4330  brxp  4675  brab2a  4697  brab2ga  4719  eqbrriv  4739  eqbrrdv  4741  eqbrrdiv  4742  opeliunxp2  4785  opelco2g  4813  opelco  4817  cnvss  4818  elcnv2  4823  opelcnvg  4825  brcnvg  4826  dfdm3  4832  dfrn3  4834  elrng  4836  eldm2g  4841  breldm  4849  dmopab  4856  opelrng  4877  opelrn  4879  elrn  4888  rnopab  4892  brres  4931  brresg  4933  resieq  4935  opelresi  4936  resiexg  4970  iss  4971  dfres2  4977  restidsing  4981  dfima3  4991  elima3  4995  imai  5002  elimasn  5013  eliniseg  5016  cotr  5028  issref  5029  cnvsym  5030  intasym  5031  asymref  5032  intirr  5033  codir  5035  qfto  5036  poirr2  5039  dmsnm  5112  coiun  5156  co02  5160  coi1  5162  dffun4  5246  dffun4f  5251  funeu2  5261  funopab  5270  funco  5275  funcnvsn  5280  isarep1  5321  fnop  5338  fneu2  5340  brprcneu  5527  dffv3g  5530  tz6.12  5562  nfvres  5568  0fv  5570  funopfv  5576  fnopfvb  5578  fvmptss2  5612  funfvbrb  5650  dff3im  5682  dff4im  5683  f1ompt  5688  idref  5778  foeqcnvco  5812  f1eqcocnv  5813  fliftel  5815  fliftel1  5816  fliftcnv  5817  f1oiso  5848  ovprc  5931  brabvv  5942  1st2ndbr  6209  xporderlem  6256  opeliunxp2f  6263  rbropapd  6267  ottposg  6280  dftpos3  6287  dftpos4  6288  tposoprab  6305  tfrlem7  6342  tfrexlem  6359  ercnv  6580  brdifun  6586  swoord1  6588  swoord2  6589  0er  6593  elecg  6599  iinerm  6633  brecop  6651  idssen  6803  xpcomco  6852  netap  7283  2omotaplemap  7286  exmidapne  7289  ltdfpr  7535  xrlenlt  8052  aprcl  8633  frecuzrdgtcl  10443  frecuzrdgfunlem  10450  climcau  11387  divides  11828  isstructim  12526  isstructr  12527  imasaddfnlemg  12791  subrgdvds  13582  aprval  13598  lmrcl  14148  lmff  14206  xmeterval  14392  eldvap  14608  dvef  14645