Description: Obsolete version 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 | ⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ } | |
| Assertion | 1strbasOLD | ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 = ( Base ‘ 𝐺 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1str.g | ⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ } | |
| 2 | 1 | 1strstr | ⊢ 𝐺 Struct ⟨ 1 , 1 ⟩ |
| 3 | baseid | ⊢ Base = Slot ( Base ‘ ndx ) | |
| 4 | 1 | eqimss2i | ⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ } ⊆ 𝐺 |
| 5 | 2 3 4 | strfv | ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 = ( Base ‘ 𝐺 ) ) |