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 ⊢ Ⅎ 𝑥 𝐴
Assertion nfuni Ⅎ 𝑥 ∪ 𝐴

Proof

Step Hyp Ref Expression
1 nfuni.1 ⊢ Ⅎ 𝑥 𝐴
2 id ⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 𝐴 )
3 2 nfunid ⊢ ( Ⅎ 𝑥 𝐴 → Ⅎ 𝑥 ∪ 𝐴 )
4 1 3 ax-mp ⊢ Ⅎ 𝑥 ∪ 𝐴