Theorem eqab

Description: One direction of eqabb is provable from fewer axioms. (Contributed by Wolf Lammen, 13-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		abid1	⊢ 𝐴 = { 𝑥 ∣ 𝑥 ∈ 𝐴 }
2		abbi	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝜑 ) → { 𝑥 ∣ 𝑥 ∈ 𝐴 } = { 𝑥 ∣ 𝜑 } )
3	1 2	eqtrid	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ 𝜑 ) → 𝐴 = { 𝑥 ∣ 𝜑 } )