(copying my answer, something odd seems to have happened to the first post)
The first assumption ( A = B -> ( ps <-> ch ) ) is the idiomatic way to say that ch is the result of substituting A for B in ps, and there are many theorems that produce results of this form. The theorem is still true when you only have a one-directional implication (in fact the first step of the proof is to weaken it to one), but users of the theorem will normally have the biconditional on hand so it is more convenient to write it that way to make the theorems more interoperable. This theorem is true in any classical logic, so it holds in both NF and ZFC. (It does not hold in iset.mm, which uses intuitionistic logic, because there is a case distinction on A = B in this theorem.) New Foundations is an axiomatic system with a lot in common with ZFC, and basic theorems like this will be true in both. On Fri, Sep 29, 2023 at 11:46 PM [email protected] <[email protected]> wrote: > Theorem pm2.61ne is the following: > > Hypotheses: > pm2.61ne.1 |- ( A = B -> ( ps <-> ch ) ) > pm2.61ne.2 |- ( ( ph and A =/= B ) -> ps ) > pm2.61ne/3 |- ( ph -> ch ) > > Assertion: > pm2.61ne |- ( ph -> ps ) > > Question 1. Why isn't the first hypothesis given in the weaker condition: > > pm2.61ne.1weaker |- ( A = B -> ( ch -> ps ) ) > > Question 2. How does this "new foundations" fit in with metamath? It seems > like "new foundations" is being mixed together with "zfc foundation". For > example, Theorem msqge0 that asserts A in R -> 0 <= A * A uses pm2.61ne in > its proof. > > -- > 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/4765307e-2a18-40aa-a754-7591522e4305n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/4765307e-2a18-40aa-a754-7591522e4305n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSs%3Dz1XsXK2AZs%3DD%3Dj-eg%2Bewt%3DyB%2B0pqDakKURFwrfHCrA%40mail.gmail.com.
