Metamath Proof Explorer


Theorem nfuni

Description: Bound-variable hypothesis builder for union. (Contributed by NM, 30-Dec-1996) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Hypothesis nfuni.1 _xA
Assertion nfuni _xA

Proof

Step Hyp Ref Expression
1 nfuni.1 _xA
2 id _xA_xA
3 2 nfunid _xA_xA
4 1 3 ax-mp _xA