Metamath Proof Explorer

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 x ∃! x φ


Step Hyp Ref Expression
1 df-eu ∃! x φ x φ * x φ
2 nfe1 x x φ
3 nfmo1 x * x φ
4 2 3 nfan x x φ * x φ
5 1 4 nfxfr x ∃! x φ