Theorem abeqabi

Description: Generalized condition for a class abstraction to be equal to some class. (Contributed by RP, 2-Sep-2024)

	Ref	Expression
Hypothesis	abeqabi.a	⊢ 𝐴 = { 𝑥 ∣ 𝜓 }
Assertion	abeqabi	⊢ ( { 𝑥 ∣ 𝜑 } = 𝐴 ↔ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		abeqabi.a	⊢ 𝐴 = { 𝑥 ∣ 𝜓 }
2	1	eqeq2i	⊢ ( { 𝑥 ∣ 𝜑 } = 𝐴 ↔ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } )
3		abbib	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) )
4	2 3	bitri	⊢ ( { 𝑥 ∣ 𝜑 } = 𝐴 ↔ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) )