Re: [Metamath] Question on Theorem pm2.61ne

[Mario Carneiro]

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.)

On Fri, Sep 29, 2023 at 11:31 PM bil...@gmail.com <bil...@gmail.com> wrote:

Theorem pm2.61ne is:

● pm2.61ne.1

|- ( A = B -> ( ps <-> ch ) )

● pm2.61ne.2

|- ( ( ph /\ A =/= B ) -> ps )

● pm2.61ne.3

|- ( ph -> ch )

pm2.61ne

|- ( ph -> ps )

Question 1. Why isn't the first premise weakened to: ( A = B -> ( ch -> ps ) )

Question 2. Is this is a "new foundation" theorem rather than a "zfc theorem"? Why is is being used in the proof of Theorem msqge0 which asserts ( A in R -> 0 <= ( A * A )) ?

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/8119ecde-1c93-4caf-92fc-f2efe2c0772cn%40googlegroups.com.