On Thu, Jun 20, 2019 at 8:29 AM Mario Carneiro <[email protected]> wrote:
> so in the theorem
>
> a∈{X|P}↔a∈X∧P(a)
>
> we must have that a is a variable disjoint from X, or else we would be
> able to derive a contradiction.
>
Actually I should amend this statement; it's fine if X has an a in it,
because this theorem has no binding operators to begin with. The important
part is that any a in X is bound in outer scope.
Mario
--
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/CAFXXJSseudt0tXihQp83MCnzfFtqAhDpqN0wASHSsFa8CFM2FQ%40mail.gmail.com.
