Description: Remove from spcimdv dependency on ax-7 , ax-8 , ax-10 ,
ax-11 , ax-12ax-13 , ax-ext , df-cleq , df-clab (and
df-nfc , df-v , df-or , df-tru , df-nf ) at the price of
adding a disjoint variable condition on x , B (but in usages, x
is typically a dummy, hence fresh, variable). For the version without
this disjoint variable condition, see bj-spcimdv . (Contributed by BJ, 3-Nov-2021)(Proof modification is discouraged.)