Metamath Proof Explorer

Theorem nfreu

Description: Bound-variable hypothesis builder for restricted unique existence. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfreuw when possible. (Contributed by NM, 30-Oct-2010) (Revised by Mario Carneiro, 8-Oct-2016) (New usage is discouraged.)

Ref Expression
Hypotheses nfreu.1 _ x A
nfreu.2 x φ
Assertion nfreu x ∃! y A φ


Step Hyp Ref Expression
1 nfreu.1 _ x A
2 nfreu.2 x φ
3 nftru y
4 1 a1i _ x A
5 2 a1i x φ
6 3 4 5 nfreud x ∃! y A φ
7 6 mptru x ∃! y A φ