Please pardon me for this rather basic question. I have read https://us.metamath.org/mpeuni/mmset.html, especially on the sections "The Axioms", "The Theory of Classes". I have basic knowledge on set theory and classical logic, so I understand all the black symbols in prepositional and predicate, but I still find it difficult to understand some expressions in definitions.
For example, in https://us.metamath.org/mpeuni/df-grp.html: Grp = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)} I know that Mnd, Base, +g, 0g etc. are all classes. But I don't get what it means for ∀𝑎 ∈ (Base‘𝑔) to be next to ∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘ 𝑔) What background knowledge am I still missing out which I should be reading, or did I miss out some material already on https://us.metamath.org/mpeuni/mmset.html? Please help me by pointing me to relevant reading material.. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/ef11fbc4-7c45-42bd-a982-06b714fa9aecn%40googlegroups.com.
