Theorem nfunidALT

Description: Deduction version of nfuni . (Contributed by NM, 19-Nov-2020) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		nfunidALT.1	|- ( ph -> F/_ x A )
2		abidnf	|- ( F/_ x A -> { y | A. x y e. A } = A )
3	2	unieqd	|- ( F/_ x A -> U. { y | A. x y e. A } = U. A )
4		nfaba1	|- F/_ x { y | A. x y e. A }
5	4	nfuni	|- F/_ x U. { y | A. x y e. A }
6	1 3 5	nfded	|- ( ph -> F/_ x U. A )