Theorem nfunidALT2

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

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

Proof

Step	Hyp	Ref	Expression
1		nfunidALT2.1	|- ( ph -> F/_ x A )
2		nfaba1	|- F/_ x { y | A. x y e. A }
3	2	nfuni	|- F/_ x U. { y | A. x y e. A }
4		nfnfc1	|- F/ x F/_ x A
5		abidnf	|- ( F/_ x A -> { y | A. x y e. A } = A )
6	5	unieqd	|- ( F/_ x A -> U. { y | A. x y e. A } = U. A )
7	4 6	nfceqdf	|- ( F/_ x A -> ( F/_ x U. { y | A. x y e. A } <-> F/_ x U. A ) )
8	1 7	syl	|- ( ph -> ( F/_ x U. { y | A. x y e. A } <-> F/_ x U. A ) )
9	3 8	mpbii	|- ( ph -> F/_ x U. A )