![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-br | GIF 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 A and/or B 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 4543). (Contributed by NM, 31-Dec-1993.) |
Ref | Expression |
---|---|
df-br | ⊢ (A𝑅B ↔ 〈A, B〉 ∈ 𝑅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class A | |
2 | cB | . . 3 class B | |
3 | cR | . . 3 class 𝑅 | |
4 | 1, 2, 3 | wbr 3755 | . 2 wff A𝑅B |
5 | 1, 2 | cop 3370 | . . 3 class 〈A, B〉 |
6 | 5, 3 | wcel 1390 | . 2 wff 〈A, B〉 ∈ 𝑅 |
7 | 4, 6 | wb 98 | 1 wff (A𝑅B ↔ 〈A, B〉 ∈ 𝑅) |
Colors of variables: wff set class |
This definition is referenced by: breq 3757 breq1 3758 breq2 3759 ssbrd 3796 nfbrd 3798 brun 3801 brin 3802 brdif 3803 opabss 3812 brabsb 3989 brabga 3992 epelg 4018 pofun 4040 brxp 4318 brab2a 4336 brab2ga 4358 eqbrriv 4378 eqbrrdv 4380 eqbrrdiv 4381 opeliunxp2 4419 opelco2g 4446 opelco 4450 cnvss 4451 elcnv2 4456 opelcnvg 4458 brcnvg 4459 dfdm3 4465 dfrn3 4467 elrng 4469 eldm2g 4474 breldm 4482 dmopab 4489 opelrng 4509 opelrn 4511 elrn 4520 rnopab 4524 brres 4561 brresg 4563 resieq 4565 opelresi 4566 resiexg 4596 iss 4597 dfres2 4601 dfima3 4614 elima3 4618 imai 4624 elimasn 4635 eliniseg 4638 cotr 4649 issref 4650 cnvsym 4651 intasym 4652 asymref 4653 intirr 4654 codir 4656 qfto 4657 poirr2 4660 dmsnm 4729 coiun 4773 co02 4777 coi1 4779 dffun4 4856 dffun4f 4861 funeu2 4870 funopab 4878 funco 4883 funcnvsn 4888 isarep1 4928 fnop 4945 fneu2 4947 brprcneu 5114 dffv3g 5117 tz6.12 5144 nfvres 5149 0fv 5151 funopfv 5156 fnopfvb 5158 fvmptss2 5190 funfvbrb 5223 dff3im 5255 dff4im 5256 f1ompt 5263 idref 5339 foeqcnvco 5373 f1eqcocnv 5374 fliftel 5376 fliftel1 5377 fliftcnv 5378 f1oiso 5408 ovprc 5482 brabvv 5493 1st2ndbr 5752 xporderlem 5793 isprmpt2 5799 ottposg 5811 dftpos3 5818 dftpos4 5819 tposoprab 5836 tfrlem7 5874 tfrexlem 5889 ercnv 6063 brdifun 6069 swoord1 6071 swoord2 6072 0er 6076 elecg 6080 iinerm 6114 brecop 6132 idssen 6193 xpcomco 6236 ltdfpr 6489 xrlenlt 6881 frecuzrdgfn 8879 |
Copyright terms: Public domain | W3C validator |