Theorem elab6g

Description: Membership in a class abstraction. Class version of sb6 . (Contributed by SN, 5-Oct-2024)

	Ref	Expression
Assertion	elab6g	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝐴 ∈ { 𝑥 ∣ 𝜑 } ) )
2		eqeq2	⊢ ( 𝑦 = 𝐴 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝐴 ) )
3	2	imbi1d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑥 = 𝑦 → 𝜑 ) ↔ ( 𝑥 = 𝐴 → 𝜑 ) ) )
4	3	albidv	⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) )
5		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
6		sb6	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
7	5 6	bitri	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
8	1 4 7	vtoclbg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) )