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  5633  dffv3g  5636  tz6.12  5668  nfvres  5676  0fv  5678  funopfv  5684  fnopfvb  5686  fvmptss2  5722  funfvbrb  5761  dff3im  5793  dff4im  5794  f1ompt  5799  idref  5900  foeqcnvco  5934  f1eqcocnv  5935  fliftel  5937  fliftel1  5938  fliftcnv  5939  f1oiso  5970  ovprc  6057  brabvv  6070  1st2ndbr  6350  xporderlem  6399  opeliunxp2f  6407  rbropapd  6411  ottposg  6424  dftpos3  6431  dftpos4  6432  tposoprab  6449  tfrlem7  6486  tfrexlem  6503  ercnv  6726  brdifun  6732  swoord1  6734  swoord2  6735  0er  6739  elecg  6745  iinerm  6779  brecop  6797  idssen  6953  xpcomco  7013  netap  7476  2omotaplemap  7479  exmidapne  7482  ltdfpr  7729  xrlenlt  8247  aprcl  8829  frecuzrdgtcl  10678  frecuzrdgfunlem  10685  climcau  11928  divides  12371  isstructim  13117  isstructr  13118  imasaddfnlemg  13418  subrgdvds  14271  aprval  14318  lmrcl  14943  lmff  15000  xmeterval  15186  eldvap  15433  dvef  15478  iswlk  16201  wlkv  16204  wlkcprim  16228  wlklenvclwlk  16251  trlsv  16262  istrl  16263  eupthv  16324  iseupth  16325