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	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nfuni	$$⊢\underset{\_}{Ⅎ}x\bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		nfuni.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		id	$$⊢\underset{\_}{Ⅎ}xA\to \underset{\_}{Ⅎ}xA$$
3	2	nfunid	$$⊢\underset{\_}{Ⅎ}xA\to \underset{\_}{Ⅎ}x\bigcup A$$
4	1 3	ax-mp	$$⊢\underset{\_}{Ⅎ}x\bigcup A$$