Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-br | Unicode version |
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. This definition of relations 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 (see for example iprc 4777). (Contributed by NM, 31-Dec-1993.) |
Ref | Expression |
---|---|
df-br |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cB | . . 3 | |
3 | cR | . . 3 | |
4 | 1, 2, 3 | wbr 3899 | . 2 |
5 | 1, 2 | cop 3500 | . . 3 |
6 | 5, 3 | wcel 1465 | . 2 |
7 | 4, 6 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: breq 3901 breq1 3902 breq2 3903 ssbrd 3941 nfbrd 3943 br0 3946 brne0 3947 brm 3948 brun 3949 brin 3950 brdif 3951 opabss 3962 brabsb 4153 brabga 4156 epelg 4182 pofun 4204 brxp 4540 brab2a 4562 brab2ga 4584 eqbrriv 4604 eqbrrdv 4606 eqbrrdiv 4607 opeliunxp2 4649 opelco2g 4677 opelco 4681 cnvss 4682 elcnv2 4687 opelcnvg 4689 brcnvg 4690 dfdm3 4696 dfrn3 4698 elrng 4700 eldm2g 4705 breldm 4713 dmopab 4720 opelrng 4741 opelrn 4743 elrn 4752 rnopab 4756 brres 4795 brresg 4797 resieq 4799 opelresi 4800 resiexg 4834 iss 4835 dfres2 4841 dfima3 4854 elima3 4858 imai 4865 elimasn 4876 eliniseg 4879 cotr 4890 issref 4891 cnvsym 4892 intasym 4893 asymref 4894 intirr 4895 codir 4897 qfto 4898 poirr2 4901 dmsnm 4974 coiun 5018 co02 5022 coi1 5024 dffun4 5104 dffun4f 5109 funeu2 5119 funopab 5128 funco 5133 funcnvsn 5138 isarep1 5179 fnop 5196 fneu2 5198 brprcneu 5382 dffv3g 5385 tz6.12 5417 nfvres 5422 0fv 5424 funopfv 5429 fnopfvb 5431 fvmptss2 5464 funfvbrb 5501 dff3im 5533 dff4im 5534 f1ompt 5539 idref 5626 foeqcnvco 5659 f1eqcocnv 5660 fliftel 5662 fliftel1 5663 fliftcnv 5664 f1oiso 5695 ovprc 5774 brabvv 5785 1st2ndbr 6050 xporderlem 6096 opeliunxp2f 6103 rbropapd 6107 ottposg 6120 dftpos3 6127 dftpos4 6128 tposoprab 6145 tfrlem7 6182 tfrexlem 6199 ercnv 6418 brdifun 6424 swoord1 6426 swoord2 6427 0er 6431 elecg 6435 iinerm 6469 brecop 6487 idssen 6639 xpcomco 6688 ltdfpr 7282 xrlenlt 7797 aprcl 8375 frecuzrdgtcl 10140 frecuzrdgfunlem 10147 climcau 11071 divides 11407 isstructim 11884 isstructr 11885 lmrcl 12271 lmff 12329 xmeterval 12515 eldvap 12731 dvef 12767 |
Copyright terms: Public domain | W3C validator |