Definition df-br 2617

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 2616	. 2 wff ARB
5	1, 2	cop 2409	. . 3 class <.A, B>.
6	5, 3	wcel 957	. 2 wff <.A, B>. e. R
7	4, 6	wb 146	1 wff (ARB <-> <.A, B>. e. R)

This definition is referenced by:  breq 2618  breq1 2619  breq2 2620  ssbrd 2653  hbbr 2655  brprc 2658  opabss 2665  brabsb 2813  brabg 2815  brrelex 3204  brxp 3212  brelg 3219  brinxp2 3228  eqbrriv 3249  opelxpex2 3276  brco 3286  opelcog 3287  cnvss 3288  elcnv2 3291  opelcnvg 3293  brcnvg 3294  cnvco 3297  dfdm3 3299  dfrn3 3301  eldm2 3305  breldm 3312  opelrn 3342  elrn 3347  dmcoss 3360  brres 3370  resieq 3373  resiexg 3393  iss 3394  dfima2 3402  dfima3 3403  elima3 3407  imai 3414  eliniseg 3426  cotr 3433  cnvsym 3434  intasym 3435  asymref 3436  intirr 3438  cnvi 3444  rninxp 3479  co02 3505  coi1 3507  coass 3509  dffun4 3525  dffun5 3526  funeu2 3535  dffun7 3537  funopab 3545  funin 3563  isarep1 3574  fnop 3588  fneu2 3590  fcoi1 3642  fcoi2 3643  tz6.12 3734  funopfv 3748  fnopfvb 3751  funopfvb 3753  fvopab5 3790  dff2 3814  dff3 3815  fvi 3839  f1oiso 3901  oprprc1 3981  dfec2 4261  brecop 4303  ecopoprdm 4306  brsdom 4376  brdom2 4382  idssen 4400  sbthcl 4452  brsdom2 4454  aceq3lem 4719  brdom3 4788  brdom7disj 4791  brdom6disj 4792  ltpiord 5002  ltxrt 5482  xrlenltt 5488  eltopsp 7583  tpsex 7584  ismsg 7779  isring 8126  avril1 8768  helloworld 8770

Copyright terms: Public domain