Description: Obsolete proof of 1strbas as of 15-Nov-2024. The base set of a constructed one-slot structure. (Contributed by AV, 27-Mar-2020) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | 1str.g | |- G = { <. ( Base ` ndx ) , B >. } |
|
| Assertion | 1strbasOLD | |- ( B e. V -> B = ( Base ` G ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1str.g | |- G = { <. ( Base ` ndx ) , B >. } |
|
| 2 | 1 | 1strstr | |- G Struct <. 1 , 1 >. |
| 3 | baseid | |- Base = Slot ( Base ` ndx ) |
|
| 4 | 1 | eqimss2i | |- { <. ( Base ` ndx ) , B >. } C_ G |
| 5 | 2 3 4 | strfv | |- ( B e. V -> B = ( Base ` G ) ) |