Description: Version of axrep4 with a disjoint variable condition, requiring fewer axioms. (Contributed by Matthew House, 18-Sep-2025)