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	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
Assertion	nfunidALT	⊢ ( 𝜑 → Ⅎ 𝑥 ∪ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nfunidALT.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
2		abidnf	⊢ ( Ⅎ 𝑥 𝐴 → { 𝑦 ∣ ∀ 𝑥 𝑦 ∈ 𝐴 } = 𝐴 )
3	2	unieqd	⊢ ( Ⅎ 𝑥 𝐴 → ∪ { 𝑦 ∣ ∀ 𝑥 𝑦 ∈ 𝐴 } = ∪ 𝐴 )
4		nfaba1	⊢ Ⅎ 𝑥 { 𝑦 ∣ ∀ 𝑥 𝑦 ∈ 𝐴 }
5	4	nfuni	⊢ Ⅎ 𝑥 ∪ { 𝑦 ∣ ∀ 𝑥 𝑦 ∈ 𝐴 }
6	1 3 5	nfded	⊢ ( 𝜑 → Ⅎ 𝑥 ∪ 𝐴 )