Theorem nfeu1ALT

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.)

	Ref	Expression
Assertion	nfeu1ALT	|- F/ x E! x ph

Proof

Step	Hyp	Ref	Expression
1		df-eu	|- ( E! x ph <-> ( E. x ph /\ E* x ph ) )
2		nfe1	|- F/ x E. x ph
3		nfmo1	|- F/ x E* x ph
4	2 3	nfan	|- F/ x ( E. x ph /\ E* x ph )
5	1 4	nfxfr	|- F/ x E! x ph