Description: Version of axc11 with a disjoint variable condition, which does not
require ax-13 nor ax-10 . Remark: the following theorems ( hbae ,
nfae , hbnae , nfnae , hbnaes ) would need to be totally
unbundled to be proved without ax-13 , hence would be simple
consequences of ax-5 or nfv . (Contributed by BJ, 31-May-2019)(Proof modification is discouraged.)