![]() |
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 3806 |
. 2
![]() ![]() ![]() ![]() |
5 | 1, 2 | cop 3420 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5, 3 | wcel 1434 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 4, 6 | wb 103 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: breq 3808 breq1 3809 breq2 3810 ssbrd 3847 nfbrd 3849 brun 3852 brin 3853 brdif 3854 opabss 3863 brabsb 4045 brabga 4048 epelg 4074 pofun 4096 brxp 4422 brab2a 4440 brab2ga 4462 eqbrriv 4482 eqbrrdv 4484 eqbrrdiv 4485 opeliunxp2 4525 opelco2g 4552 opelco 4556 cnvss 4557 elcnv2 4562 opelcnvg 4564 brcnvg 4565 dfdm3 4571 dfrn3 4573 elrng 4575 eldm2g 4580 breldm 4588 dmopab 4595 opelrng 4615 opelrn 4617 elrn 4626 rnopab 4630 brres 4667 brresg 4669 resieq 4671 opelresi 4672 resiexg 4704 iss 4705 dfres2 4709 dfima3 4722 elima3 4726 imai 4732 elimasn 4743 eliniseg 4746 cotr 4757 issref 4758 cnvsym 4759 intasym 4760 asymref 4761 intirr 4762 codir 4764 qfto 4765 poirr2 4768 dmsnm 4837 coiun 4881 co02 4885 coi1 4887 dffun4 4964 dffun4f 4969 funeu2 4978 funopab 4986 funco 4991 funcnvsn 4996 isarep1 5037 fnop 5054 fneu2 5056 brprcneu 5224 dffv3g 5227 tz6.12 5255 nfvres 5260 0fv 5262 funopfv 5267 fnopfvb 5269 fvmptss2 5301 funfvbrb 5334 dff3im 5366 dff4im 5367 f1ompt 5374 idref 5450 foeqcnvco 5483 f1eqcocnv 5484 fliftel 5486 fliftel1 5487 fliftcnv 5488 f1oiso 5518 ovprc 5593 brabvv 5604 1st2ndbr 5863 xporderlem 5905 isprmpt2 5914 ottposg 5926 dftpos3 5933 dftpos4 5934 tposoprab 5951 tfrlem7 5988 tfrexlem 6005 ercnv 6216 brdifun 6222 swoord1 6224 swoord2 6225 0er 6229 elecg 6233 iinerm 6267 brecop 6285 idssen 6347 xpcomco 6393 ltdfpr 6835 xrlenlt 7321 frecuzrdgtcl 9571 frecuzrdgfunlem 9578 climcau 10410 divides 10430 |
Copyright terms: Public domain | W3C validator |