![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > breqi | Structured version Visualization version Unicode version |
Description: Equality inference for binary relations. (Contributed by NM, 19-Feb-2005.) |
Ref | Expression |
---|---|
breqi.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
breqi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breqi.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | breq 4420 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-ex 1675 df-cleq 2455 df-clel 2458 df-br 4419 |
This theorem is referenced by: f1ompt 6072 isocnv3 6253 brtpos2 7010 brwitnlem 7240 brdifun 7421 omxpenlem 7704 infxpenlem 8475 ltpiord 9343 nqerf 9386 nqerid 9389 ordpinq 9399 ltxrlt 9735 ltxr 11449 trclublem 13114 oduleg 16433 oduposb 16437 meet0 16438 join0 16439 xmeterval 21502 pi1cpbl 22130 ltgov 24698 brbtwn 24985 rgraprop 25712 rusgraprop 25713 rusgrargra 25714 avril1 25956 axhcompl-zf 26707 hlimadd 26902 hhcmpl 26909 hhcms 26912 hlim0 26944 fcoinvbr 28268 posrasymb 28470 trleile 28479 isarchi 28550 pstmfval 28750 pstmxmet 28751 lmlim 28804 brtxp 30697 brpprod 30702 brpprod3b 30704 brtxpsd2 30712 brdomain 30750 brrange 30751 brimg 30754 brapply 30755 brsuccf 30758 brrestrict 30766 brub 30771 brlb 30772 colineardim1 30878 broutsideof 30938 fneval 31058 relowlpssretop 31813 phpreu 31975 poimirlem26 32012 brnonrel 36241 climreeq 37779 rgrprop 39724 rusgrprop 39726 gte-lte 40813 gt-lt 40814 gte-lteh 40815 gt-lth 40816 |
Copyright terms: Public domain | W3C validator |