Definition df-br 4034

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 4934). (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 4033	. 2 wff A R B
5	1, 2	cop 3625	. . 3 class <. A , B >.
6	5, 3	wcel 2167	. 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  4035  breq1  4036  breq2  4037  ssbrd  4076  nfbrd  4078  br0  4081  brne0  4082  brm  4083  brun  4084  brin  4085  brdif  4086  opabss  4097  brabsb  4295  brabga  4298  epelg  4325  pofun  4347  brxp  4694  brab2a  4716  brab2ga  4738  eqbrriv  4758  eqbrrdv  4760  eqbrrdiv  4761  opeliunxp2  4806  opelco2g  4834  opelco  4838  cnvss  4839  elcnv2  4844  opelcnvg  4846  brcnvg  4847  dfdm3  4853  dfrn3  4855  elrng  4857  eldm2g  4862  breldm  4870  dmopab  4877  opelrng  4898  opelrn  4900  elrn  4909  rnopab  4913  brres  4952  brresg  4954  resieq  4956  opelresi  4957  resiexg  4991  iss  4992  dfres2  4998  restidsing  5002  dfima3  5012  elima3  5016  imai  5025  elimasn  5036  eliniseg  5039  cotr  5051  issref  5052  cnvsym  5053  intasym  5054  asymref  5055  intirr  5056  codir  5058  qfto  5059  poirr2  5062  dmsnm  5135  coiun  5179  co02  5183  coi1  5185  dffun4  5269  dffun4f  5274  funeu2  5284  funopab  5293  funco  5298  funcnvsn  5303  isarep1  5344  fnop  5361  fneu2  5363  brprcneu  5551  dffv3g  5554  tz6.12  5586  nfvres  5592  0fv  5594  funopfv  5600  fnopfvb  5602  fvmptss2  5636  funfvbrb  5675  dff3im  5707  dff4im  5708  f1ompt  5713  idref  5803  foeqcnvco  5837  f1eqcocnv  5838  fliftel  5840  fliftel1  5841  fliftcnv  5842  f1oiso  5873  ovprc  5957  brabvv  5968  1st2ndbr  6242  xporderlem  6289  opeliunxp2f  6296  rbropapd  6300  ottposg  6313  dftpos3  6320  dftpos4  6321  tposoprab  6338  tfrlem7  6375  tfrexlem  6392  ercnv  6613  brdifun  6619  swoord1  6621  swoord2  6622  0er  6626  elecg  6632  iinerm  6666  brecop  6684  idssen  6836  xpcomco  6885  netap  7321  2omotaplemap  7324  exmidapne  7327  ltdfpr  7573  xrlenlt  8091  aprcl  8673  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  climcau  11512  divides  11954  isstructim  12692  isstructr  12693  imasaddfnlemg  12957  subrgdvds  13791  aprval  13838  lmrcl  14427  lmff  14485  xmeterval  14671  eldvap  14918  dvef  14963