Theorem eluniab

Description: Membership in union of a class abstraction. (Contributed by NM, 11-Aug-1994) (Revised by Mario Carneiro, 14-Nov-2016)

	Ref	Expression
Assertion	eluniab	⊢ ( 𝐴 ∈ ∪ { 𝑥 ∣ 𝜑 } ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		eluni	⊢ ( 𝐴 ∈ ∪ { 𝑥 ∣ 𝜑 } ↔ ∃ 𝑦 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) )
2		nfv	⊢ Ⅎ 𝑥 𝐴 ∈ 𝑦
3		nfsab1	⊢ Ⅎ 𝑥 𝑦 ∈ { 𝑥 ∣ 𝜑 }
4	2 3	nfan	⊢ Ⅎ 𝑥 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ∈ { 𝑥 ∣ 𝜑 } )
5		nfv	⊢ Ⅎ 𝑦 ( 𝐴 ∈ 𝑥 ∧ 𝜑 )
6		eleq2w	⊢ ( 𝑦 = 𝑥 → ( 𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑥 ) )
7		eleq1w	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑥 ∈ { 𝑥 ∣ 𝜑 } ) )
8		abid	⊢ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 )
9	7 8	bitrdi	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 ) )
10	6 9	anbi12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝐴 ∈ 𝑦 ∧ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) ↔ ( 𝐴 ∈ 𝑥 ∧ 𝜑 ) ) )
11	4 5 10	cbvexv1	⊢ ( ∃ 𝑦 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ 𝜑 ) )
12	1 11	bitri	⊢ ( 𝐴 ∈ ∪ { 𝑥 ∣ 𝜑 } ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ 𝜑 ) )