Theorem elunirab

Description: Membership in union of a class abstraction. (Contributed by NM, 4-Oct-2006)

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

Proof

Step	Hyp	Ref	Expression
1		eluniab	⊢ ( 𝐴 ∈ ∪ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
2		df-rab	⊢ { 𝑥 ∈ 𝐵 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) }
3	2	unieqi	⊢ ∪ { 𝑥 ∈ 𝐵 ∣ 𝜑 } = ∪ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) }
4	3	eleq2i	⊢ ( 𝐴 ∈ ∪ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ 𝐴 ∈ ∪ { 𝑥 ∣ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) } )
5		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝐴 ∈ 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝐴 ∈ 𝑥 ∧ 𝜑 ) ) )
6		an12	⊢ ( ( 𝑥 ∈ 𝐵 ∧ ( 𝐴 ∈ 𝑥 ∧ 𝜑 ) ) ↔ ( 𝐴 ∈ 𝑥 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
7	6	exbii	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ ( 𝐴 ∈ 𝑥 ∧ 𝜑 ) ) ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
8	5 7	bitri	⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝐴 ∈ 𝑥 ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
9	1 4 8	3bitr4i	⊢ ( 𝐴 ∈ ∪ { 𝑥 ∈ 𝐵 ∣ 𝜑 } ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐴 ∈ 𝑥 ∧ 𝜑 ) )