Metamath Proof Explorer

Theorem nfeud2

Description: Bound-variable hypothesis builder for uniqueness. Usage of this theorem is discouraged because it depends on ax-13 . Check out nfeudw for a version that replaces the distinctor with a disjoint variable condition, not requiring ax-13 . (Contributed by Mario Carneiro, 14-Nov-2016) (Proof shortened by Wolf Lammen, 4-Oct-2018) (Proof shortened by BJ, 14-Oct-2022) (New usage is discouraged.)

Ref Expression
Hypotheses nfeud2.1 y φ
nfeud2.2 φ ¬ x x = y x ψ
Assertion nfeud2 φ x ∃! y ψ


Step Hyp Ref Expression
1 nfeud2.1 y φ
2 nfeud2.2 φ ¬ x x = y x ψ
3 df-eu ∃! y ψ y ψ * y ψ
4 1 2 nfexd2 φ x y ψ
5 1 2 nfmod2 φ x * y ψ
6 4 5 nfand φ x y ψ * y ψ
7 3 6 nfxfrd φ x ∃! y ψ