Definition df-br 2626

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 such as "<" that compares two classes A and B, which might be numbers such as 1 and 2. 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.

Assertion

Ref	Expression
df-br	|- (ARB <-> <.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 2625	. 2 wff ARB
5	1, 2	cop 2416	. . 3 class <.A, B>.
6	5, 3	wcel 960	. 2 wff <.A, B>. e. R
7	4, 6	wb 146	1 wff (ARB <-> <.A, B>. e. R)

This definition is referenced by:  breq 2627  breq1 2628  breq2 2629  ssbrd 2662  hbbr 2664  brprc 2667  opabss 2674  brabsb 2823  brabg 2825  brrelex 3214  brxp 3222  brelg 3229  brinxp2 3238  eqbrriv 3259  opelxpex2 3286  brco 3296  opelcog 3297  cnvss 3298  elcnv2 3301  opelcnvg 3303  brcnvg 3304  cnvco 3307  dfdm3 3309  dfrn3 3311  eldm2 3315  breldm 3322  opelrn 3352  elrn 3357  dmcoss 3370  brres 3380  resieq 3383  resiexg 3403  iss 3404  dfima2 3412  dfima3 3413  elima3 3417  imai 3424  eliniseg 3436  cotr 3443  cnvsym 3444  intasym 3445  asymref 3446  intirr 3448  cnvi 3454  rninxp 3489  co02 3515  coi1 3517  coass 3519  dffun4 3535  dffun5 3536  funeu2 3545  dffun7 3547  funopab 3555  funin 3573  isarep1 3584  fnop 3598  fneu2 3600  fcoi1 3652  fcoi2 3653  tz6.12 3744  funopfv 3758  fnopfvb 3761  funopfvb 3763  fvopab5 3800  dff2 3824  dff3 3825  fvi 3849  f1oiso 3911  oprprc1 3991  dfec2 4271  brecop 4313  ecopoprdm 4316  brsdom 4388  brdom2 4395  idssen 4413  sbthcl 4466  brsdom2 4468  aceq3lem 4749  brdom3 4818  brdom7disj 4821  brdom6disj 4822  ltpiord 5034  ltxrt 5514  xrlenltt 5520  eltopsp 7612  tpsex 7613  ismsg 7804  isring 8144  avril1 8786  helloworld 8788

Copyright terms: Public domain