| Description: Substitution of variable
in universal quantifier. Closed form of
sb8mo 2504.
This theorem relates to wl-mo3t 33358, since replacing  with
    ![]](rbrack.gif "]") in
the latter yields subexpressions like
, which can be reduced to via sbft 2379
and sbco 2412. So  
is provable from
wl-mo3t 33358 in a simple fashion, unfortunately only if
and are
known to be distinct. To avoid any hassle with distinctors, we prefer
to derive this theorem independently, ignoring the close connection
between both theorems. From an educational standpoint, one would assume
wl-mo3t 33358 to be more fundamental, as it hints how the
"at most one"
objects on both sides of the biconditional correlate (they are the
same), if they exist at all, and then prove this theorem from it.
(Contributed by Wolf Lammen, 11-Aug-2019.) |
