Definition df-br 4031

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 4931). (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 4030	. 2 wff A R B
5	1, 2	cop 3622	. . 3 class <. A , B >.
6	5, 3	wcel 2164	. 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  4032  breq1  4033  breq2  4034  ssbrd  4073  nfbrd  4075  br0  4078  brne0  4079  brm  4080  brun  4081  brin  4082  brdif  4083  opabss  4094  brabsb  4292  brabga  4295  epelg  4322  pofun  4344  brxp  4691  brab2a  4713  brab2ga  4735  eqbrriv  4755  eqbrrdv  4757  eqbrrdiv  4758  opeliunxp2  4803  opelco2g  4831  opelco  4835  cnvss  4836  elcnv2  4841  opelcnvg  4843  brcnvg  4844  dfdm3  4850  dfrn3  4852  elrng  4854  eldm2g  4859  breldm  4867  dmopab  4874  opelrng  4895  opelrn  4897  elrn  4906  rnopab  4910  brres  4949  brresg  4951  resieq  4953  opelresi  4954  resiexg  4988  iss  4989  dfres2  4995  restidsing  4999  dfima3  5009  elima3  5013  imai  5022  elimasn  5033  eliniseg  5036  cotr  5048  issref  5049  cnvsym  5050  intasym  5051  asymref  5052  intirr  5053  codir  5055  qfto  5056  poirr2  5059  dmsnm  5132  coiun  5176  co02  5180  coi1  5182  dffun4  5266  dffun4f  5271  funeu2  5281  funopab  5290  funco  5295  funcnvsn  5300  isarep1  5341  fnop  5358  fneu2  5360  brprcneu  5548  dffv3g  5551  tz6.12  5583  nfvres  5589  0fv  5591  funopfv  5597  fnopfvb  5599  fvmptss2  5633  funfvbrb  5672  dff3im  5704  dff4im  5705  f1ompt  5710  idref  5800  foeqcnvco  5834  f1eqcocnv  5835  fliftel  5837  fliftel1  5838  fliftcnv  5839  f1oiso  5870  ovprc  5954  brabvv  5965  1st2ndbr  6239  xporderlem  6286  opeliunxp2f  6293  rbropapd  6297  ottposg  6310  dftpos3  6317  dftpos4  6318  tposoprab  6335  tfrlem7  6372  tfrexlem  6389  ercnv  6610  brdifun  6616  swoord1  6618  swoord2  6619  0er  6623  elecg  6629  iinerm  6663  brecop  6681  idssen  6833  xpcomco  6882  netap  7316  2omotaplemap  7319  exmidapne  7322  ltdfpr  7568  xrlenlt  8086  aprcl  8667  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  climcau  11493  divides  11935  isstructim  12635  isstructr  12636  imasaddfnlemg  12900  subrgdvds  13734  aprval  13781  lmrcl  14370  lmff  14428  xmeterval  14614  eldvap  14861  dvef  14906