Description: Bound-variable hypothesis builder for uniqueness. See nfeu1ALT for a
shorter proof using ax-12 . This proof illustrates the systematic way
of proving nonfreeness in a defined expression: consider the definiens as
a tree whose nodes are its subformulas, and prove by tree-induction the
nonfreeness of each node, starting from the leaves (generally using nfv or nf* theorems for previously defined expressions) and up to the root.
Here, the definiens is a conjunction of two previously defined
expressions, which automatically yields the present proof. (Contributed by NM, 9-Jul-1994)(Revised by Mario Carneiro, 7-Oct-2016)(Revised by BJ, 2-Oct-2022)(Proof modification is discouraged.)