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

Proof

Step	Hyp	Ref	Expression
1		nfunidALT2.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
2		nfaba1	⊢ Ⅎ 𝑥 { 𝑦 ∣ ∀ 𝑥 𝑦 ∈ 𝐴 }
3	2	nfuni	⊢ Ⅎ 𝑥 ∪ { 𝑦 ∣ ∀ 𝑥 𝑦 ∈ 𝐴 }
4		nfnfc1	⊢ Ⅎ 𝑥 Ⅎ 𝑥 𝐴
5		abidnf	⊢ ( Ⅎ 𝑥 𝐴 → { 𝑦 ∣ ∀ 𝑥 𝑦 ∈ 𝐴 } = 𝐴 )
6	5	unieqd	⊢ ( Ⅎ 𝑥 𝐴 → ∪ { 𝑦 ∣ ∀ 𝑥 𝑦 ∈ 𝐴 } = ∪ 𝐴 )
7	4 6	nfceqdf	⊢ ( Ⅎ 𝑥 𝐴 → ( Ⅎ 𝑥 ∪ { 𝑦 ∣ ∀ 𝑥 𝑦 ∈ 𝐴 } ↔ Ⅎ 𝑥 ∪ 𝐴 ) )
8	1 7	syl	⊢ ( 𝜑 → ( Ⅎ 𝑥 ∪ { 𝑦 ∣ ∀ 𝑥 𝑦 ∈ 𝐴 } ↔ Ⅎ 𝑥 ∪ 𝐴 ) )
9	3 8	mpbii	⊢ ( 𝜑 → Ⅎ 𝑥 ∪ 𝐴 )