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