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 
|- F/_ x A
Assertion nfuni 
|- F/_ x U. A

Proof

Step Hyp Ref Expression
1 nfuni.1 
 |-  F/_ x A
2 id 
 |-  ( F/_ x A -> F/_ x A )
3 2 nfunid 
 |-  ( F/_ x A -> F/_ x U. A )
4 1 3 ax-mp 
 |-  F/_ x U. A