Theorem nfunid

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

	Ref	Expression
Hypothesis	nfunid.3	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
Assertion	nfunid	⊢ ( 𝜑 → Ⅎ 𝑥 ∪ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nfunid.3	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
2		dfuni2	⊢ ∪ 𝐴 = { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 ∈ 𝑧 }
3		nfv	⊢ Ⅎ 𝑦 𝜑
4		nfv	⊢ Ⅎ 𝑧 𝜑
5		nfvd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 ∈ 𝑧 )
6	4 1 5	nfrexd	⊢ ( 𝜑 → Ⅎ 𝑥 ∃ 𝑧 ∈ 𝐴 𝑦 ∈ 𝑧 )
7	3 6	nfabdw	⊢ ( 𝜑 → Ⅎ 𝑥 { 𝑦 ∣ ∃ 𝑧 ∈ 𝐴 𝑦 ∈ 𝑧 } )
8	2 7	nfcxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 ∪ 𝐴 )