df-br - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Definition df-br 2610

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

normally denotes a relation such as "

" that compares two classes

and

, which might be numbers such as

and

. This definition is well-defined, although not very meaningful, when classes

and/or

are proper classes (i.e. are not sets). On the other hand, we often find uses for this definition when

is a proper class.

**Assertion**
Ref	Expression
df-br

**Detailed syntax breakdown of Definition df-br**
Step	Hyp	Ref	Expression
1		cA	. . 3
2		cB	. . 3
3		cR	. . 3
4	1, 2, 3	wbr 2609	. 2
5	1, 2	cop 2401	. . 3
6	5, 3	wcel 955	. 2
7	4, 6	wb 146	1

Colors of variables: wff set class

This definition is referenced by: breq 2611 breq1 2612 breq2 2613 ssbrd 2646 hbbr 2648 brprc 2651 opabss 2658 brabsb 2805 brabg 2807 brrelex 3197 brxp 3205 brelg 3212 brinxp2 3221 eqbrriv 3242 brco 3278 opelcog 3279 cnvss 3280 elcnv2 3283 opelcnvg 3285 brcnvg 3286 cnvco 3289 dfdm3 3291 dfrn3 3293 eldm2 3297 breldm 3304 opelrn 3333 elrn 3336 dmcoss 3347 brres 3357 resieq 3360 resiexg 3380 iss 3381 dfima2 3389 dfima3 3390 elima3 3394 imai 3401 eliniseg 3413 cotr 3420 cnvsym 3421 intasym 3422 asymref 3423 asymrefOLD 3425 intirr 3427 cnvi 3433 rninxp 3468 co02 3494 coi1 3496 coass 3498 dffun4 3514 dffun5 3515 funeu2 3524 dffun7 3526 funopab 3534 funin 3552 isarep1 3563 fnop 3577 fneu2 3579 fcoi1 3630 fcoi2 3631 tz6.12 3722 funopfv 3736 fnopfvb 3739 funopfvb 3741 fvopab5 3778 dff2 3802 dff3 3803 fvi 3827 f1oiso 3889 oprprc1 3969 dfec2 4248 brecop 4290 ecopoprdm 4293 brsdom 4363 brdom2 4369 idssen 4387 sbthcl 4439 brsdom2 4441 aceq3lem 4704 brdom3 4773 brdom7disj 4776 brdom6disj 4777 ltpiord 4987 ltxrt 5467 xrlenltt 5473 eltopsp 7546 tpsex 7547 ismsg 7739 isring 8078 isvcgOLD 8133 avril1 8723 helloworld 8725