Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > breq | Unicode version |
Description: Equality theorem for binary relations. (Contributed by NM, 4-Jun-1995.) |
Ref | Expression |
---|---|
breq |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq2 2234 | . 2 | |
2 | df-br 3990 | . 2 | |
3 | df-br 3990 | . 2 | |
4 | 1, 2, 3 | 3bitr4g 222 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wceq 1348 wcel 2141 cop 3586 class class class wbr 3989 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-4 1503 ax-17 1519 ax-ial 1527 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 df-clel 2166 df-br 3990 |
This theorem is referenced by: breqi 3995 breqd 4000 poeq1 4284 soeq1 4300 frforeq1 4328 weeq1 4341 fveq1 5495 foeqcnvco 5769 f1eqcocnv 5770 isoeq2 5781 isoeq3 5782 ofreq 6064 supeq3 6967 shftfvalg 10782 shftfval 10785 pw1nct 14036 |
Copyright terms: Public domain | W3C validator |