Definition df-br 4006

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 4897). (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 4005	. 2 wff A R B
5	1, 2	cop 3597	. . 3 class <. A , B >.
6	5, 3	wcel 2148	. 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  4007  breq1  4008  breq2  4009  ssbrd  4048  nfbrd  4050  br0  4053  brne0  4054  brm  4055  brun  4056  brin  4057  brdif  4058  opabss  4069  brabsb  4263  brabga  4266  epelg  4292  pofun  4314  brxp  4659  brab2a  4681  brab2ga  4703  eqbrriv  4723  eqbrrdv  4725  eqbrrdiv  4726  opeliunxp2  4769  opelco2g  4797  opelco  4801  cnvss  4802  elcnv2  4807  opelcnvg  4809  brcnvg  4810  dfdm3  4816  dfrn3  4818  elrng  4820  eldm2g  4825  breldm  4833  dmopab  4840  opelrng  4861  opelrn  4863  elrn  4872  rnopab  4876  brres  4915  brresg  4917  resieq  4919  opelresi  4920  resiexg  4954  iss  4955  dfres2  4961  restidsing  4965  dfima3  4975  elima3  4979  imai  4986  elimasn  4997  eliniseg  5000  cotr  5012  issref  5013  cnvsym  5014  intasym  5015  asymref  5016  intirr  5017  codir  5019  qfto  5020  poirr2  5023  dmsnm  5096  coiun  5140  co02  5144  coi1  5146  dffun4  5229  dffun4f  5234  funeu2  5244  funopab  5253  funco  5258  funcnvsn  5263  isarep1  5304  fnop  5321  fneu2  5323  brprcneu  5510  dffv3g  5513  tz6.12  5545  nfvres  5550  0fv  5552  funopfv  5557  fnopfvb  5559  fvmptss2  5593  funfvbrb  5631  dff3im  5663  dff4im  5664  f1ompt  5669  idref  5759  foeqcnvco  5793  f1eqcocnv  5794  fliftel  5796  fliftel1  5797  fliftcnv  5798  f1oiso  5829  ovprc  5912  brabvv  5923  1st2ndbr  6187  xporderlem  6234  opeliunxp2f  6241  rbropapd  6245  ottposg  6258  dftpos3  6265  dftpos4  6266  tposoprab  6283  tfrlem7  6320  tfrexlem  6337  ercnv  6558  brdifun  6564  swoord1  6566  swoord2  6567  0er  6571  elecg  6575  iinerm  6609  brecop  6627  idssen  6779  xpcomco  6828  netap  7255  2omotaplemap  7258  exmidapne  7261  ltdfpr  7507  xrlenlt  8024  aprcl  8605  frecuzrdgtcl  10414  frecuzrdgfunlem  10421  climcau  11357  divides  11798  isstructim  12478  isstructr  12479  imasaddfnlemg  12740  subrgdvds  13361  aprval  13377  lmrcl  13730  lmff  13788  xmeterval  13974  eldvap  14190  dvef  14227