Definition df-br 4103

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 5017). (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 4102	. 2 wff A R B
5	1, 2	cop 3685	. . 3 class <. A , B >.
6	5, 3	wcel 2203	. 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  4104  breq1  4105  breq2  4106  ssbrd  4145  nfbrd  4148  br0  4151  brne0  4152  brm  4153  brun  4154  brin  4155  brdif  4156  opabss  4167  brabsb  4370  brabga  4373  epelg  4402  pofun  4424  brxp  4771  brab2a  4794  brab2ga  4816  eqbrriv  4836  eqbrrdv  4838  eqbrrdiv  4839  opeliunxp2  4886  opelco2g  4914  opelco  4918  cnvss  4919  elcnv2  4924  opelcnvg  4926  brcnvg  4927  dfdm3  4933  dfrn3  4935  elrng  4937  eldm2g  4943  breldm  4951  dmopab  4958  opelrng  4980  opelrn  4982  elrn  4991  rnopab  4995  brres  5035  brresg  5037  resieq  5039  opelresi  5040  resiexg  5074  iss  5075  dfres2  5081  restidsing  5085  dfima3  5095  elima3  5099  imai  5109  elimasn  5120  eliniseg  5123  cotr  5135  issref  5136  cnvsym  5137  intasym  5138  asymref  5139  intirr  5140  codir  5142  qfto  5143  poirr2  5146  dmsnm  5219  coiun  5263  co02  5267  coi1  5269  dffun4  5354  dffun4f  5359  funeu2  5369  funopab  5378  funco  5383  funcnvsn  5392  isarep1  5433  fnop  5452  fneu2  5454  brprcneu  5654  dffv3g  5657  tz6.12  5689  nfvres  5697  0fv  5699  funopfv  5705  fnopfvb  5707  fvmptss2  5743  funfvbrb  5782  dff3im  5813  dff4im  5814  f1ompt  5819  idref  5920  foeqcnvco  5954  f1eqcocnv  5955  fliftel  5957  fliftel1  5958  fliftcnv  5959  f1oiso  5990  ovprc  6077  brabvv  6090  1st2ndbr  6369  xporderlem  6418  cnvimadfsn  6436  opeliunxp2f  6460  rbropapd  6464  ottposg  6477  dftpos3  6484  dftpos4  6485  tposoprab  6502  tfrlem7  6539  tfrexlem  6556  ercnv  6779  brdifun  6785  swoord1  6787  swoord2  6788  0er  6792  elecg  6798  iinerm  6832  brecop  6850  idssen  7007  xpcomco  7068  netap  7556  2omotaplemap  7559  exmidapne  7562  ltdfpr  7809  xrlenlt  8326  aprcl  8908  frecuzrdgtcl  10760  frecuzrdgfunlem  10767  climcau  12010  divides  12453  isstructim  13200  isstructr  13201  imasaddfnlemg  13501  subrgdvds  14354  aprval  14402  lmrcl  15027  lmff  15084  xmeterval  15270  eldvap  15517  dvef  15562  iswlk  16288  wlkv  16291  wlkcprim  16315  wlklenvclwlk  16338  trlsv  16349  istrl  16350  eupthv  16411  iseupth  16412