Definition df-br 3938

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 4815). (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 3937	. 2 wff A R B
5	1, 2	cop 3535	. . 3 class <. A , B >.
6	5, 3	wcel 1481	. 2 wff <. A , B >. e. R
7	4, 6	wb 104	1 wff ( A R B <-> <. A , B >. e. R )

This definition is referenced by:  breq  3939  breq1  3940  breq2  3941  ssbrd  3979  nfbrd  3981  br0  3984  brne0  3985  brm  3986  brun  3987  brin  3988  brdif  3989  opabss  4000  brabsb  4191  brabga  4194  epelg  4220  pofun  4242  brxp  4578  brab2a  4600  brab2ga  4622  eqbrriv  4642  eqbrrdv  4644  eqbrrdiv  4645  opeliunxp2  4687  opelco2g  4715  opelco  4719  cnvss  4720  elcnv2  4725  opelcnvg  4727  brcnvg  4728  dfdm3  4734  dfrn3  4736  elrng  4738  eldm2g  4743  breldm  4751  dmopab  4758  opelrng  4779  opelrn  4781  elrn  4790  rnopab  4794  brres  4833  brresg  4835  resieq  4837  opelresi  4838  resiexg  4872  iss  4873  dfres2  4879  dfima3  4892  elima3  4896  imai  4903  elimasn  4914  eliniseg  4917  cotr  4928  issref  4929  cnvsym  4930  intasym  4931  asymref  4932  intirr  4933  codir  4935  qfto  4936  poirr2  4939  dmsnm  5012  coiun  5056  co02  5060  coi1  5062  dffun4  5142  dffun4f  5147  funeu2  5157  funopab  5166  funco  5171  funcnvsn  5176  isarep1  5217  fnop  5234  fneu2  5236  brprcneu  5422  dffv3g  5425  tz6.12  5457  nfvres  5462  0fv  5464  funopfv  5469  fnopfvb  5471  fvmptss2  5504  funfvbrb  5541  dff3im  5573  dff4im  5574  f1ompt  5579  idref  5666  foeqcnvco  5699  f1eqcocnv  5700  fliftel  5702  fliftel1  5703  fliftcnv  5704  f1oiso  5735  ovprc  5814  brabvv  5825  1st2ndbr  6090  xporderlem  6136  opeliunxp2f  6143  rbropapd  6147  ottposg  6160  dftpos3  6167  dftpos4  6168  tposoprab  6185  tfrlem7  6222  tfrexlem  6239  ercnv  6458  brdifun  6464  swoord1  6466  swoord2  6467  0er  6471  elecg  6475  iinerm  6509  brecop  6527  idssen  6679  xpcomco  6728  ltdfpr  7338  xrlenlt  7853  aprcl  8432  frecuzrdgtcl  10216  frecuzrdgfunlem  10223  climcau  11148  divides  11531  isstructim  12012  isstructr  12013  lmrcl  12399  lmff  12457  xmeterval  12643  eldvap  12859  dvef  12896