HomeTheorem List (p. 11 of 11)
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List
| Home |
brismu
bridi Theorem List (p. 11 of 11) |
< Previous Wrap >
|
|
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List | ||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Axiom | ax-vusyselbri-titla 1001 | Automatically generated axiom: {titla} is {vusyselbri} |
| vusyselbri titla | ||
| Axiom | ax-xumselbri-cidro 1002 | Automatically generated axiom: {cidro} is {xumselbri} |
| xumselbri cidro | ||
| Axiom | ax-xumselbri-cnisa 1003 | Automatically generated axiom: {cnisa} is {xumselbri} |
| xumselbri cnisa | ||
| Axiom | ax-xumselbri-kijno 1004 | Automatically generated axiom: {kijno} is {xumselbri} |
| xumselbri kijno | ||
| Axiom | ax-xumselbri-margu 1005 | Automatically generated axiom: {margu} is {xumselbri} |
| xumselbri margu | ||
| Axiom | ax-xumselbri-nikle 1006 | Automatically generated axiom: {nikle} is {xumselbri} |
| xumselbri nikle | ||
| Axiom | ax-xumselbri-rijno 1007 | Automatically generated axiom: {rijno} is {xumselbri} |
| xumselbri rijno | ||
| Axiom | ax-xumselbri-sliri 1008 | Automatically generated axiom: {sliri} is {xumselbri} |
| xumselbri sliri | ||
| Axiom | ax-xumselbri-solji 1009 | Automatically generated axiom: {solji} is {xumselbri} |
| xumselbri solji | ||
| Axiom | ax-xumselbri-tabno 1010 | Automatically generated axiom: {tabno} is {xumselbri} |
| xumselbri tabno | ||
| Axiom | ax-xumselbri-tinci 1011 | Automatically generated axiom: {tinci} is {xumselbri} |
| xumselbri tinci | ||
| Axiom | ax-xumselbri-tirse 1012 | Automatically generated axiom: {tirse} is {xumselbri} |
| xumselbri tirse | ||
| Axiom | ax-xumselbri-trano 1013 | Automatically generated axiom: {trano} is {xumselbri} |
| xumselbri trano | ||
| Axiom | ax-xumselbri-tunka 1014 | Automatically generated axiom: {tunka} is {xumselbri} |
| xumselbri tunka | ||
| Axiom | ax-xumselbri-zinki 1015 | Automatically generated axiom: {zinki} is {xumselbri} |
| xumselbri zinki | ||
| Axiom | ax-xumsleselbri-djacu 1016 | Automatically generated axiom: {djacu} is {xumsleselbri} |
| xumsleselbri djacu | ||
| Axiom | ax-gumri-mledi 1017 | Automatically generated axiom: {gumri} is a subrelation of {mledi} |
| ⊢ pa ka ce'u gumri ce'u ki'irni'i pa ka ce'u mledi ce'u | ||
| Axiom | ax-kuhurkupresu-ckunu 1018 | Automatically generated axiom: {ku'urkupresu} is a subrelation of {ckunu} |
| ⊢ pa ka ce'u ku'urkupresu ce'u ki'irni'i pa ka ce'u ckunu ce'u | ||
| Axiom | ax-bambu-srasu 1019 | Automatically generated axiom: {bambu} is a subrelation of {srasu} |
| ⊢ pa ka ce'u bambu ce'u ki'irni'i pa ka ce'u srasu ce'u | ||
| Axiom | ax-cindu-spati 1020 | Automatically generated axiom: {cindu} is a subrelation of {spati} |
| ⊢ pa ka ce'u cindu ce'u ki'irni'i pa ka ce'u spati ce'u | ||
| Axiom | ax-ckunu-spati 1021 | Automatically generated axiom: {ckunu} is a subrelation of {spati} |
| ⊢ pa ka ce'u ckunu ce'u ki'irni'i pa ka ce'u spati ce'u | ||
| Axiom | ax-lelxe-spati 1022 | Automatically generated axiom: {lelxe} is a subrelation of {spati} |
| ⊢ pa ka ce'u lelxe ce'u ki'irni'i pa ka ce'u spati ce'u | ||
| Axiom | ax-marna-spati 1023 | Automatically generated axiom: {marna} is a subrelation of {spati} |
| ⊢ pa ka ce'u marna ce'u ki'irni'i pa ka ce'u spati ce'u | ||
| Axiom | ax-nimre-spati 1024 | Automatically generated axiom: {nimre} is a subrelation of {spati} |
| ⊢ pa ka ce'u nimre ce'u ki'irni'i pa ka ce'u spati ce'u | ||
| Axiom | ax-poplu-spati 1025 | Automatically generated axiom: {poplu} is a subrelation of {spati} |
| ⊢ pa ka ce'u poplu ce'u ki'irni'i pa ka ce'u spati ce'u | ||
| Axiom | ax-rozgu-spati 1026 | Automatically generated axiom: {rozgu} is a subrelation of {spati} |
| ⊢ pa ka ce'u rozgu ce'u ki'irni'i pa ka ce'u spati ce'u | ||
| Axiom | ax-sluni-spati 1027 | Automatically generated axiom: {sluni} is a subrelation of {spati} |
| ⊢ pa ka ce'u sluni ce'u ki'irni'i pa ka ce'u spati ce'u | ||
| Axiom | ax-srasu-spati 1028 | Automatically generated axiom: {srasu} is a subrelation of {spati} |
| ⊢ pa ka ce'u srasu ce'u ki'irni'i pa ka ce'u spati ce'u | ||
| Axiom | ax-tujli-spati 1029 | Automatically generated axiom: {tujli} is a subrelation of {spati} |
| ⊢ pa ka ce'u tujli ce'u ki'irni'i pa ka ce'u spati ce'u | ||
| Axiom | ax-xruba-spati 1030 | Automatically generated axiom: {xruba} is a subrelation of {spati} |
| ⊢ pa ka ce'u xruba ce'u ki'irni'i pa ka ce'u spati ce'u | ||
| Axiom | ax-since-respa 1031 | Automatically generated axiom: {since} is a subrelation of {respa} |
| ⊢ pa ka ce'u since ce'u ki'irni'i pa ka ce'u respa ce'u | ||
| Axiom | ax-respa-danlu 1032 | Automatically generated axiom: {respa} is a subrelation of {danlu} |
| ⊢ pa ka ce'u respa ce'u ki'irni'i pa ka ce'u danlu ce'u | ||
| Axiom | ax-remna-smani 1033 | Automatically generated axiom: {remna} is a subrelation of {smani} |
| ⊢ pa ka ce'u remna ce'u ki'irni'i pa ka ce'u smani ce'u | ||
| Axiom | ax-smani-mabru 1034 | Automatically generated axiom: {smani} is a subrelation of {mabru} |
| ⊢ pa ka ce'u smani ce'u ki'irni'i pa ka ce'u mabru ce'u | ||
| Axiom | ax-tirxu-mlatu 1035 | Automatically generated axiom: {tirxu} is a subrelation of {mlatu} |
| ⊢ pa ka ce'u tirxu ce'u ki'irni'i pa ka ce'u mlatu ce'u | ||
| Axiom | ax-cinfo-mlatu 1036 | Automatically generated axiom: {cinfo} is a subrelation of {mlatu} |
| ⊢ pa ka ce'u cinfo ce'u ki'irni'i pa ka ce'u mlatu ce'u | ||
| Axiom | ax-mlatu-mabru 1037 | Automatically generated axiom: {mlatu} is a subrelation of {mabru} |
| ⊢ pa ka ce'u mlatu ce'u ki'irni'i pa ka ce'u mabru ce'u | ||
| Axiom | ax-xanto-mabru 1038 | Automatically generated axiom: {xanto} is a subrelation of {mabru} |
| ⊢ pa ka ce'u xanto ce'u ki'irni'i pa ka ce'u mabru ce'u | ||
| Axiom | ax-xasli-mabru 1039 | Automatically generated axiom: {xasli} is a subrelation of {mabru} |
| ⊢ pa ka ce'u xasli ce'u ki'irni'i pa ka ce'u mabru ce'u | ||
| Axiom | ax-xirma-mabru 1040 | Automatically generated axiom: {xirma} is a subrelation of {mabru} |
| ⊢ pa ka ce'u xirma ce'u ki'irni'i pa ka ce'u mabru ce'u | ||
| Axiom | ax-xarju-mabru 1041 | Automatically generated axiom: {xarju} is a subrelation of {mabru} |
| ⊢ pa ka ce'u xarju ce'u ki'irni'i pa ka ce'u mabru ce'u | ||
| Axiom | ax-ractu-mabru 1042 | Automatically generated axiom: {ractu} is a subrelation of {mabru} |
| ⊢ pa ka ce'u ractu ce'u ki'irni'i pa ka ce'u mabru ce'u | ||
| Axiom | ax-smacu-mabru 1043 | Automatically generated axiom: {smacu} is a subrelation of {mabru} |
| ⊢ pa ka ce'u smacu ce'u ki'irni'i pa ka ce'u mabru ce'u | ||
| Axiom | ax-kumte-mabru 1044 | Automatically generated axiom: {kumte} is a subrelation of {mabru} |
| ⊢ pa ka ce'u kumte ce'u ki'irni'i pa ka ce'u mabru ce'u | ||
| Axiom | ax-mirli-mabru 1045 | Automatically generated axiom: {mirli} is a subrelation of {mabru} |
| ⊢ pa ka ce'u mirli ce'u ki'irni'i pa ka ce'u mabru ce'u | ||
| Axiom | ax-cribe-mabru 1046 | Automatically generated axiom: {cribe} is a subrelation of {mabru} |
| ⊢ pa ka ce'u cribe ce'u ki'irni'i pa ka ce'u mabru ce'u | ||
| Axiom | ax-ratcu-mabru 1047 | Automatically generated axiom: {ratcu} is a subrelation of {mabru} |
| ⊢ pa ka ce'u ratcu ce'u ki'irni'i pa ka ce'u mabru ce'u | ||
| Axiom | ax-labno-gerku 1048 | Automatically generated axiom: {labno} is a subrelation of {gerku} |
| ⊢ pa ka ce'u labno ce'u ki'irni'i pa ka ce'u gerku ce'u | ||
| Axiom | ax-lorxu-gerku 1049 | Automatically generated axiom: {lorxu} is a subrelation of {gerku} |
| ⊢ pa ka ce'u lorxu ce'u ki'irni'i pa ka ce'u gerku ce'u | ||
| Axiom | ax-gerku-mabru 1050 | Automatically generated axiom: {gerku} is a subrelation of {mabru} |
| ⊢ pa ka ce'u gerku ce'u ki'irni'i pa ka ce'u mabru ce'u | ||
| Axiom | ax-banfi-danlu 1051 | Automatically generated axiom: {banfi} is a subrelation of {danlu} |
| ⊢ pa ka ce'u banfi ce'u ki'irni'i pa ka ce'u danlu ce'u | ||
| Axiom | ax-finpe-danlu 1052 | Automatically generated axiom: {finpe} is a subrelation of {danlu} |
| ⊢ pa ka ce'u finpe ce'u ki'irni'i pa ka ce'u danlu ce'u | ||
| Axiom | ax-curnu-danlu 1053 | Automatically generated axiom: {curnu} is a subrelation of {danlu} |
| ⊢ pa ka ce'u curnu ce'u ki'irni'i pa ka ce'u danlu ce'u | ||
| Axiom | ax-gunse-cipni 1054 | Automatically generated axiom: {gunse} is a subrelation of {cipni} |
| ⊢ pa ka ce'u gunse ce'u ki'irni'i pa ka ce'u cipni ce'u | ||
| Axiom | ax-jipci-cipni 1055 | Automatically generated axiom: {jipci} is a subrelation of {cipni} |
| ⊢ pa ka ce'u jipci ce'u ki'irni'i pa ka ce'u cipni ce'u | ||
| Axiom | ax-xruki-cipni 1056 | Automatically generated axiom: {xruki} is a subrelation of {cipni} |
| ⊢ pa ka ce'u xruki ce'u ki'irni'i pa ka ce'u cipni ce'u | ||
| Axiom | ax-datka-cipni 1057 | Automatically generated axiom: {datka} is a subrelation of {cipni} |
| ⊢ pa ka ce'u datka ce'u ki'irni'i pa ka ce'u cipni ce'u | ||
| Axiom | ax-cipni-danlu 1058 | Automatically generated axiom: {cipni} is a subrelation of {danlu} |
| ⊢ pa ka ce'u cipni ce'u ki'irni'i pa ka ce'u danlu ce'u | ||
| Axiom | ax-toldi-cinki 1059 | Automatically generated axiom: {toldi} is a subrelation of {cinki} |
| ⊢ pa ka ce'u toldi ce'u ki'irni'i pa ka ce'u cinki ce'u | ||
| Axiom | ax-jukni-cinki 1060 | Automatically generated axiom: {jukni} is a subrelation of {cinki} |
| ⊢ pa ka ce'u jukni ce'u ki'irni'i pa ka ce'u cinki ce'u | ||
| Axiom | ax-manti-cinki 1061 | Automatically generated axiom: {manti} is a subrelation of {cinki} |
| ⊢ pa ka ce'u manti ce'u ki'irni'i pa ka ce'u cinki ce'u | ||
| Axiom | ax-sfani-cinki 1062 | Automatically generated axiom: {sfani} is a subrelation of {cinki} |
| ⊢ pa ka ce'u sfani ce'u ki'irni'i pa ka ce'u cinki ce'u | ||
| Axiom | ax-jalra-cinki 1063 | Automatically generated axiom: {jalra} is a subrelation of {cinki} |
| ⊢ pa ka ce'u jalra ce'u ki'irni'i pa ka ce'u cinki ce'u | ||
| Axiom | ax-civla-cinki 1064 | Automatically generated axiom: {civla} is a subrelation of {cinki} |
| ⊢ pa ka ce'u civla ce'u ki'irni'i pa ka ce'u cinki ce'u | ||
| Axiom | ax-bifce-cinki 1065 | Automatically generated axiom: {bifce} is a subrelation of {cinki} |
| ⊢ pa ka ce'u bifce ce'u ki'irni'i pa ka ce'u cinki ce'u | ||
| Axiom | ax-cinki-danlu 1066 | Automatically generated axiom: {cinki} is a subrelation of {danlu} |
| ⊢ pa ka ce'u cinki ce'u ki'irni'i pa ka ce'u danlu ce'u | ||
| Axiom | ax-lanme-bakni 1067 | Automatically generated axiom: {lanme} is a subrelation of {bakni} |
| ⊢ pa ka ce'u lanme ce'u ki'irni'i pa ka ce'u bakni ce'u | ||
| Axiom | ax-kanba-bakni 1068 | Automatically generated axiom: {kanba} is a subrelation of {bakni} |
| ⊢ pa ka ce'u kanba ce'u ki'irni'i pa ka ce'u bakni ce'u | ||
| Axiom | ax-bakni-mabru 1069 | Automatically generated axiom: {bakni} is a subrelation of {mabru} |
| ⊢ pa ka ce'u bakni ce'u ki'irni'i pa ka ce'u mabru ce'u | ||
| Axiom | ax-mabru-danlu 1070 | Automatically generated axiom: {mabru} is a subrelation of {danlu} |
| ⊢ pa ka ce'u mabru ce'u ki'irni'i pa ka ce'u danlu ce'u | ||
| < Previous Wrap > |
| Copyright terms: Public domain | < Previous Wrap > |