On Sunday, June 2, 2019 at 7:16:01 PM UTC+2, Thierry Arnoux wrote:
>
> "x = A -> ( ph <-> ps )"
> would be the way to state with an implicit substitution the same thing as
> “[. A / x ]. ph <-> ps”
> states explicitly, that is
> “ps is the result of taking all instances of ‘x’ in ph, and
> substituting them with ‘A’.”
>
For the record, this equivalence between implicit and explicit
substitutions, back and forth, is expressed by the two theorems
sbceq1a $p |- ( x = A -> ( ph <-> [. A / x ]. ph ) ) $=
and
$d x A $. $d x ps $. sbcie.1 $e |- A e. _V $.
sbcie.2 $e |- ( x = A -> ( ph <-> ps ) ) $.
sbcie $p |- ( [. A / x ]. ph <-> ps ) $=
Benoit
>
> My experience is that implicit substitution is more easy to work with.
> _
> Thierry
>
>
>
--
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/d19c8ebd-2d9c-4924-b798-0b3c62ec6182%40googlegroups.com.
