![]() |
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 ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-br |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cB |
. . 3
![]() ![]() | |
3 | cR |
. . 3
![]() ![]() | |
4 | 1, 2, 3 | wbr 4018 |
. 2
![]() ![]() ![]() ![]() |
5 | 1, 2 | cop 3610 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5, 3 | wcel 2160 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 4, 6 | wb 105 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: breq 4020 breq1 4021 breq2 4022 ssbrd 4061 nfbrd 4063 br0 4066 brne0 4067 brm 4068 brun 4069 brin 4070 brdif 4071 opabss 4082 brabsb 4279 brabga 4282 epelg 4308 pofun 4330 brxp 4675 brab2a 4697 brab2ga 4719 eqbrriv 4739 eqbrrdv 4741 eqbrrdiv 4742 opeliunxp2 4785 opelco2g 4813 opelco 4817 cnvss 4818 elcnv2 4823 opelcnvg 4825 brcnvg 4826 dfdm3 4832 dfrn3 4834 elrng 4836 eldm2g 4841 breldm 4849 dmopab 4856 opelrng 4877 opelrn 4879 elrn 4888 rnopab 4892 brres 4931 brresg 4933 resieq 4935 opelresi 4936 resiexg 4970 iss 4971 dfres2 4977 restidsing 4981 dfima3 4991 elima3 4995 imai 5002 elimasn 5013 eliniseg 5016 cotr 5028 issref 5029 cnvsym 5030 intasym 5031 asymref 5032 intirr 5033 codir 5035 qfto 5036 poirr2 5039 dmsnm 5112 coiun 5156 co02 5160 coi1 5162 dffun4 5246 dffun4f 5251 funeu2 5261 funopab 5270 funco 5275 funcnvsn 5280 isarep1 5321 fnop 5338 fneu2 5340 brprcneu 5527 dffv3g 5530 tz6.12 5562 nfvres 5568 0fv 5570 funopfv 5576 fnopfvb 5578 fvmptss2 5612 funfvbrb 5650 dff3im 5682 dff4im 5683 f1ompt 5688 idref 5778 foeqcnvco 5812 f1eqcocnv 5813 fliftel 5815 fliftel1 5816 fliftcnv 5817 f1oiso 5848 ovprc 5931 brabvv 5942 1st2ndbr 6209 xporderlem 6256 opeliunxp2f 6263 rbropapd 6267 ottposg 6280 dftpos3 6287 dftpos4 6288 tposoprab 6305 tfrlem7 6342 tfrexlem 6359 ercnv 6580 brdifun 6586 swoord1 6588 swoord2 6589 0er 6593 elecg 6599 iinerm 6633 brecop 6651 idssen 6803 xpcomco 6852 netap 7283 2omotaplemap 7286 exmidapne 7289 ltdfpr 7535 xrlenlt 8052 aprcl 8633 frecuzrdgtcl 10443 frecuzrdgfunlem 10450 climcau 11387 divides 11828 isstructim 12526 isstructr 12527 imasaddfnlemg 12791 subrgdvds 13582 aprval 13598 lmrcl 14148 lmff 14206 xmeterval 14392 eldvap 14608 dvef 14645 |
Copyright terms: Public domain | W3C validator |