Definition df-br 4089

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 5001). (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 4088	. 2 wff A R B
5	1, 2	cop 3672	. . 3 class <. A , B >.
6	5, 3	wcel 2202	. 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  4090  breq1  4091  breq2  4092  ssbrd  4131  nfbrd  4134  br0  4137  brne0  4138  brm  4139  brun  4140  brin  4141  brdif  4142  opabss  4153  brabsb  4355  brabga  4358  epelg  4387  pofun  4409  brxp  4756  brab2a  4779  brab2ga  4801  eqbrriv  4821  eqbrrdv  4823  eqbrrdiv  4824  opeliunxp2  4870  opelco2g  4898  opelco  4902  cnvss  4903  elcnv2  4908  opelcnvg  4910  brcnvg  4911  dfdm3  4917  dfrn3  4919  elrng  4921  eldm2g  4927  breldm  4935  dmopab  4942  opelrng  4964  opelrn  4966  elrn  4975  rnopab  4979  brres  5019  brresg  5021  resieq  5023  opelresi  5024  resiexg  5058  iss  5059  dfres2  5065  restidsing  5069  dfima3  5079  elima3  5083  imai  5092  elimasn  5103  eliniseg  5106  cotr  5118  issref  5119  cnvsym  5120  intasym  5121  asymref  5122  intirr  5123  codir  5125  qfto  5126  poirr2  5129  dmsnm  5202  coiun  5246  co02  5250  coi1  5252  dffun4  5337  dffun4f  5342  funeu2  5352  funopab  5361  funco  5366  funcnvsn  5375  isarep1  5416  fnop  5435  fneu2  5437  brprcneu  5632  dffv3g  5635  tz6.12  5667  nfvres  5675  0fv  5677  funopfv  5683  fnopfvb  5685  fvmptss2  5721  funfvbrb  5760  dff3im  5792  dff4im  5793  f1ompt  5798  idref  5897  foeqcnvco  5931  f1eqcocnv  5932  fliftel  5934  fliftel1  5935  fliftcnv  5936  f1oiso  5967  ovprc  6054  brabvv  6067  1st2ndbr  6347  xporderlem  6396  opeliunxp2f  6404  rbropapd  6408  ottposg  6421  dftpos3  6428  dftpos4  6429  tposoprab  6446  tfrlem7  6483  tfrexlem  6500  ercnv  6723  brdifun  6729  swoord1  6731  swoord2  6732  0er  6736  elecg  6742  iinerm  6776  brecop  6794  idssen  6950  xpcomco  7010  netap  7473  2omotaplemap  7476  exmidapne  7479  ltdfpr  7726  xrlenlt  8244  aprcl  8826  frecuzrdgtcl  10674  frecuzrdgfunlem  10681  climcau  11908  divides  12351  isstructim  13097  isstructr  13098  imasaddfnlemg  13398  subrgdvds  14251  aprval  14298  lmrcl  14918  lmff  14975  xmeterval  15161  eldvap  15408  dvef  15453  iswlk  16176  wlkv  16179  wlkcprim  16203  wlklenvclwlk  16226  trlsv  16237  istrl  16238  eupthv  16299  iseupth  16300