Definition df-br 4641

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. Class R normally denotes a relation that compares two classes A and B. This definition 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. (Contributed by NM, 4-Jun-1995.)

Assertion

Ref	Expression
df-br	⊢ (ARB ↔ ⟨A, B⟩ ∈ 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 4640	. 2 wff ARB
5	1, 2	cop 4562	. . 3 class ⟨A, B⟩
6	5, 3	wcel 1710	. 2 wff ⟨A, B⟩ ∈ R
7	4, 6	wb 176	1 wff (ARB ↔ ⟨A, B⟩ ∈ R)

This definition is referenced by:  breq  4642  breq1  4643  breq2  4644  ssbrd  4681  nfbrd  4683  brex  4690  brun  4693  brin  4694  brdif  4695  opelopabsb  4698  brabsb  4699  brabga  4702  br1stg  4731  dfima2  4746  dfco1  4749  dfsi2  4752  elima3  4757  opelssetsn  4761  brxp  4813  eqbrriv  4852  opelco  4885  cnvss  4886  elcnv2  4891  opelcnv  4894  elrn2  4898  eldm2  4900  dfrn3  4904  breldm  4912  dmun  4913  dmopab  4916  elimapw1  4945  opelres  4951  dfima4  4953  opelrn  4962  rnopab  4968  iss  5001  dfres2  5003  imai  5011  elimasn  5020  eliniseg  5021  cotr  5027  cnvsym  5028  intasym  5029  intirr  5030  dmsnopg  5067  rnsnop  5076  dfco2  5081  coiun  5091  co02  5093  co01  5094  dffun2  5120  dffun4  5122  dffun5  5123  funeu2  5133  funopab  5140  funsn  5148  fnop  5187  fneu2  5189  fcnvres  5244  tz6.12  5346  funopfv  5358  fnopfvb  5360  funopfvb  5362  funfvbrb  5402  fvi  5443  f1oiso  5500  opsnelsi  5775  oteltxp  5783  brimage  5794  otsnelsi3  5806  composeex  5821  addcfnex  5825  funsex  5829  fnsex  5833  dmpprod  5841  crossex  5851  pw1fnex  5853  fnfullfunlem1  5857  fvfullfunlem2  5863  domfnex  5871  ranfnex  5872  clos1ex  5877  transex  5911  refex  5912  antisymex  5913  connexex  5914  foundex  5915  extex  5916  symex  5917  elec  5965  qsexg  5983  mapexi  6004  enex  6032  idssen  6041  enpw1lem1  6062  enmap2lem1  6064  enmap1lem1  6070  enprmaplem1  6077  nenpw1pwlem1  6085  ovmuc  6131  mucex  6134  ovcelem1  6172  ceex  6175  leconnnc  6219  tcfnex  6245  nmembers1lem1  6269  nncdiv3lem1  6276  nncdiv3lem2  6277  nnc3n3p1  6279  nchoicelem3  6292  nchoicelem10  6299  nchoicelem11  6300  nchoicelem16  6305  nchoicelem18  6307  fnfreclem1  6318  fnfreclem2  6319  fnfreclem3  6320  frecsuc  6323