The specific question of what it means for two restricted quantifiers to
be next to each other is perhaps best answered by pointing to a simpler
example like https://us.metamath.org/mpeuni/r19.12.html - the ∀푦 ∈ 퐵
∃푥 ∈ 퐴 휑 there has the same syntax as ∀푎 ∈ (Base‘푔)∃푚 ∈
(Base‘푔)(푚(+g‘푔)푎) =
The ∀푎 ∈ (Base‘푔) expression, or in ascii syntax "A. a e. (Base`g)" is
the beginning of the restricted forall quantifier "A. x e. A ph" where you
have highlighted just the "A. x e. A" part. It is read "for all x in A,
..." and denotes that some property "ph" holds for every x such that x e. A
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
