Theorem clabel

Description: Membership of a class abstraction in another class. (Contributed by NM, 17-Jan-2006)

	Ref	Expression
Assertion	clabel	⊢ ( { 𝑥 ∣ 𝜑 } ∈ 𝐴 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfclel	⊢ ( { 𝑥 ∣ 𝜑 } ∈ 𝐴 ↔ ∃ 𝑦 ( 𝑦 = { 𝑥 ∣ 𝜑 } ∧ 𝑦 ∈ 𝐴 ) )
2		abeq2	⊢ ( 𝑦 = { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ 𝜑 ) )
3	2	anbi2ci	⊢ ( ( 𝑦 = { 𝑥 ∣ 𝜑 } ∧ 𝑦 ∈ 𝐴 ) ↔ ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ 𝜑 ) ) )
4	3	exbii	⊢ ( ∃ 𝑦 ( 𝑦 = { 𝑥 ∣ 𝜑 } ∧ 𝑦 ∈ 𝐴 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ 𝜑 ) ) )
5	1 4	bitri	⊢ ( { 𝑥 ∣ 𝜑 } ∈ 𝐴 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ 𝜑 ) ) )