Description: Alternate proof of nfeu1 . This 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
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 BJ, 2-Oct-2022)(Proof modification is discouraged.)(New usage is discouraged.)