Typo in description of Theorem ceqsexgv?

[billh0420]

Should "elimination" be "introduction" in the description of Theorem ceqsexgv?

If so, I will submit a pull request.

Likewise for the following theorems ceqsrexv, ceqsrexbv, ceqsrex2v.

[icecream17]

It's both (Edit: Under one interpretation. I see that "introduction" probably more intuitively refers to the hypothesis being converted into the conclusion)

If you have E. x ( x = A /\ ph ) it can be "eliminated" or converted into ps
Likewise if you have ps it can be converted into E. x ( x = A /\ ph ) i.e. "introduced".

Probably a comment like https://us.metamath.org/mpeuni/cgsexg.html or https://us.metamath.org/mpeuni/ceqsalv.html would be more accurate. So maybe: "Convert implicit substitution into explicit existential substitution"

(ceqsexv is also affected by this issue)

[billh0420]

Let's restrict to just class substitution.

For me, explicit class substitution (substituting A for x in ph) means: [. A / x ]. ph

For me, implicit class substitution (substituting A for x in ph) means: x = A -> some wff with ph.

See example theorem sbcie. Its description is: "Conversion of implicit substitution to explicit class substitution."
(Note: I would prefer: "Conversion of implicit class substitution to explicit class substitution.")

Theorem sbcie is similar to theorem ceqsexgv. Assuming A e. V, the first yields:

                 ( [. A / x ]. ph <-> ps )

while the second yields:

                ( E. x ( x = A /\ ph ) <-> ps )

I don't see the second as being explicit class substitution (according to my understanding): I see it more of introducing the existential quantifier E.

Background of why I am making a fuss: The metamath style of proof is foreign to me (where I am probably more aligned with the natural deduction style of proof). Currently, I am working on trying to understand the metamath style of proof. I am amazed that I need to come up with a ph that involves x and a ps that does not involved x and somehow show that they are logically equivalent (given that x = A). It is even worse since the "introductory" theorems about doing this are so general. To avoid that generality, I am currently working my way through the theorems that follow df-q so that I have something that is explicit. I notice that variables like x and y are introduced (which I am happy with) and existential or universal quantifiers are applied (which I am happy with). I am still not clear where that ps comes from. This is what I am working on.

[icecream17]

That makes sense. I referred to the variants https://us.metamath.org/mpeuni/sbc5.html and https://us.metamath.org/mpeuni/sbc6g.html as "substitution" since they are equivalent to substitution, but indeed practically the forward, introducing direction of the equivalence is used a lot more.

As for ps, note that what substitution does is replace one variable with something else. Here's an example from https://us.metamath.org/mpeuni/odval.html:

When you substitute away i, naturally ps does not have any i anymore. (Here it's technically [_ I / i ]_ A = B instead of [. I / i ]. ph <-> ps, but the principle still holds)

Perhaps the most common need for substitution is when a definition or function uses general lowercase setvars, and you are replacing the setvar with a specific class. https://us.metamath.org/mpeuni/elz.html is one example of this

There's probably a lot more to say on natural deduction: this page might be helpful (it is somewhat abstract though, the examples are the most concrete part) https://us.metamath.org/mpeuni/mmnatded.html