Definition df-br 4132

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 5053). (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 4131	. 2 wff A R B
5	1, 2	cop 3712	. . 3 class <. A , B >.
6	5, 3	wcel 2209	. 2 wff <. A , B >. e. R
7	4, 6	wb 105	1 wff ( A R B <-> <. A , B >. e. R )

This definition is used by:  breq  4133  breq1  4134  breq2  4135  ssbrd  4174  nfbrd  4177  br0  4180  brne0  4181  brm  4182  brun  4183  brin  4184  brdif  4185  opabss  4196  brabsb  4405  brabga  4408  epelg  4437  pofun  4459  brxp  4807  brab2a  4830  brab2ga  4852  eqbrriv  4872  eqbrrdv  4874  eqbrrdiv  4875  opeliunxp2  4922  opelco2g  4950  opelco  4954  cnvss  4955  elcnv2  4960  opelcnvg  4962  brcnvg  4963  dfdm3  4969  dfrn3  4971  elrng  4973  eldm2g  4979  breldm  4987  dmopab  4994  opelrng  5016  opelrn  5018  elrn  5027  rnopab  5031  brres  5071  brresg  5073  resieq  5075  opelresi  5076  resiexg  5111  iss  5112  dfres2  5118  restidsing  5122  dfima3  5132  elima3  5136  imai  5146  elimasn  5157  eliniseg  5160  cotr  5172  issref  5173  cnvsym  5174  intasym  5175  asymref  5176  intirr  5177  codir  5179  qfto  5180  poirr2  5183  dmsnm  5256  coiun  5300  co02  5304  coi1  5306  dffun4  5391  dffun4f  5396  funeu2  5406  funopab  5415  funco  5420  funcnvsn  5429  isarep1  5470  fnop  5489  fneu2  5491  brprcneu  5691  dffv3g  5694  tz6.12  5726  nfvres  5735  0fv  5737  funopfv  5743  fnopfvb  5745  fvmptss2  5783  funfvbrb  5825  dff3im  5856  dff4im  5857  f1ompt  5862  idref  5965  foeqcnvco  5999  f1eqcocnv  6000  fliftel  6002  fliftel1  6003  fliftcnv  6004  f1oiso  6035  ovprc  6124  brabvv  6137  1st2ndbr  6422  xporderlem  6471  cnvimadfsn  6489  opeliunxp2f  6514  rbropapd  6518  ottposg  6531  dftpos3  6538  dftpos4  6539  tposoprab  6556  tfrlem7  6593  tfrexlem  6610  ercnv  6833  brdifun  6839  swoord1  6841  swoord2  6842  0er  6846  elecg  6852  iinerm  6886  brecop  6904  idssen  7069  xpcomco  7130  netap  7626  2omotaplemap  7629  exmidapne  7632  ltdfpr  7879  xrlenlt  8396  aprcl  8982  frecuzrdgtcl  10869  frecuzrdgfunlem  10876  climcau  12137  divides  12580  isstructim  13423  isstructr  13424  imasaddfnlemg  13693  subrgdvds  14651  aprval  14699  lmrcl  15435  lmff  15492  xmeterval  15678  eldvap  15925  dvef  15970  iswlk  16786  wlkv  16789  wlkcprim  16813  wlklenvclwlk  16836  trlsv  16847  istrl  16848  eupthv  16909  iseupth  16910