Definition df-br 4002

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 4892). (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 4001	. 2 wff A R B
5	1, 2	cop 3595	. . 3 class <. A , B >.
6	5, 3	wcel 2148	. 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  4003  breq1  4004  breq2  4005  ssbrd  4044  nfbrd  4046  br0  4049  brne0  4050  brm  4051  brun  4052  brin  4053  brdif  4054  opabss  4065  brabsb  4259  brabga  4262  epelg  4288  pofun  4310  brxp  4655  brab2a  4677  brab2ga  4699  eqbrriv  4719  eqbrrdv  4721  eqbrrdiv  4722  opeliunxp2  4764  opelco2g  4792  opelco  4796  cnvss  4797  elcnv2  4802  opelcnvg  4804  brcnvg  4805  dfdm3  4811  dfrn3  4813  elrng  4815  eldm2g  4820  breldm  4828  dmopab  4835  opelrng  4856  opelrn  4858  elrn  4867  rnopab  4871  brres  4910  brresg  4912  resieq  4914  opelresi  4915  resiexg  4949  iss  4950  dfres2  4956  restidsing  4960  dfima3  4970  elima3  4974  imai  4981  elimasn  4992  eliniseg  4995  cotr  5007  issref  5008  cnvsym  5009  intasym  5010  asymref  5011  intirr  5012  codir  5014  qfto  5015  poirr2  5018  dmsnm  5091  coiun  5135  co02  5139  coi1  5141  dffun4  5224  dffun4f  5229  funeu2  5239  funopab  5248  funco  5253  funcnvsn  5258  isarep1  5299  fnop  5316  fneu2  5318  brprcneu  5505  dffv3g  5508  tz6.12  5540  nfvres  5545  0fv  5547  funopfv  5552  fnopfvb  5554  fvmptss2  5588  funfvbrb  5626  dff3im  5658  dff4im  5659  f1ompt  5664  idref  5753  foeqcnvco  5786  f1eqcocnv  5787  fliftel  5789  fliftel1  5790  fliftcnv  5791  f1oiso  5822  ovprc  5905  brabvv  5916  1st2ndbr  6180  xporderlem  6227  opeliunxp2f  6234  rbropapd  6238  ottposg  6251  dftpos3  6258  dftpos4  6259  tposoprab  6276  tfrlem7  6313  tfrexlem  6330  ercnv  6551  brdifun  6557  swoord1  6559  swoord2  6560  0er  6564  elecg  6568  iinerm  6602  brecop  6620  idssen  6772  xpcomco  6821  netap  7248  2omotaplemap  7251  exmidapne  7254  ltdfpr  7500  xrlenlt  8016  aprcl  8597  frecuzrdgtcl  10405  frecuzrdgfunlem  10412  climcau  11346  divides  11787  isstructim  12466  isstructr  12467  aprval  13239  lmrcl  13473  lmff  13531  xmeterval  13717  eldvap  13933  dvef  13970