Theorem nfunid

Description: Deduction version of nfuni . (Contributed by NM, 18-Feb-2013)

	Ref	Expression
Hypothesis	nfunid.3	|- ( ph -> F/_ x A )
Assertion	nfunid	|- ( ph -> F/_ x U. A )

Proof

Step	Hyp	Ref	Expression
1		nfunid.3	|- ( ph -> F/_ x A )
2		dfuni2	|- U. A = { y | E. z e. A y e. z }
3		nfv	|- F/ y ph
4		nfv	|- F/ z ph
5		nfvd	|- ( ph -> F/ x y e. z )
6	4 1 5	nfrexdw	|- ( ph -> F/ x E. z e. A y e. z )
7	3 6	nfabdw	|- ( ph -> F/_ x { y | E. z e. A y e. z } )
8	2 7	nfcxfrd	|- ( ph -> F/_ x U. A )