Theorem clelab

Description: Membership of a class variable in a class abstraction. (Contributed by NM, 23-Dec-1993) (Proof shortened by Wolf Lammen, 16-Nov-2019)

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

Proof

Step	Hyp	Ref	Expression
1		dfclel	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) )
2		nfv	⊢ Ⅎ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 )
3		nfv	⊢ Ⅎ 𝑥 𝑦 = 𝐴
4		nfsab1	⊢ Ⅎ 𝑥 𝑦 ∈ { 𝑥 ∣ 𝜑 }
5	3 4	nfan	⊢ Ⅎ 𝑥 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ 𝜑 } )
6		eqeq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝐴 ↔ 𝑦 = 𝐴 ) )
7		sbequ12	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
8		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
9	7 8	syl6bbr	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) )
10	6 9	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ( 𝑦 = 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) ) )
11	2 5 10	cbvexv1	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) )
12	1 11	bitr4i	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) )