Definition df-br 2693

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>. ∈ 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 2692	. 2 wff ARB
5	1, 2	cop 2469	. . 3 class <.A, B>.
6	5, 3	wcel 994	. 2 wff <.A, B>. ∈ R
7	4, 6	wb 144	1 wff (ARB ↔ <.A, B>. ∈ R)

This definition is referenced by:  breq 2694  breq1 2695  breq2 2696  ssbrd 2729  hbbr 2731  brprc 2734  brun 2735  opabss 2742  brabsb 2893  brabg 2895  posn 2928  brrelex 3290  brxp 3298  brelg 3307  brinxp2 3317  eqbrriv 3339  opelxpex2 3369  brco 3379  opelco2g 3380  cnvss 3381  elcnv2 3385  opelcnvg 3387  brcnvg 3388  cnvco 3391  dfdm3 3393  dfrn3 3395  eldm2 3399  breldm 3406  opelrn 3432  elrn 3437  dmcoss 3450  brres 3460  resieq 3463  resiexg 3486  iss 3487  dfima2 3497  dfima3 3498  elima3 3502  imai 3509  eliniseg 3521  cotr 3528  cnvsym 3529  intasym 3530  asymref 3531  intirr 3533  cnvi 3539  rninxp 3567  coiun 3608  co02 3612  coi1 3614  coass 3616  dffun4 3633  dffun5 3634  funeu2 3643  dffun8 3645  funopab 3653  funin 3671  isarep1 3683  fnop 3697  fneu2 3699  fcoi1 3752  fcoi2 3753  tz6.12 3848  funopfv 3862  fnopfvb 3865  funopfvb 3867  fvopab5 3904  dff3 3931  dff4 3932  fvi 3956  f1oiso 4018  oprprc1 4042  fparlem1 4199  fparlem2 4200  fparlem3 4201  fparlem4 4202  dfec2 4404  brecop 4447  ecopoprdm 4450  brsdom 4522  brdom2 4529  idssen 4547  sbthcl 4604  brsdom2 4606  aceq3lem 4878  brdom3 4947  brdom7disj 4950  brdom6disj 4951  ltpiord 5169  ltxr 5649  xrlenlt 5655  eltopsp 7816  tpsex 7817  ismsg 8010  isring 8382  avril1 9058  helloworld 9060  domintreflem 10766  int2rel 10770  eltids 10771  ref3w 10772  mlteqer 10789  restidsing 10805  prj1 10809  fora 10954  isdivrng 10968  opncldf1 11454  compfipin0 11493  islocfin 11567  filnetlem4 11766  isgalem 11771  gapmlem 11783

Copyright terms: Public domain