Theorem abbi1

Description: Equivalent formulas yield equal class abstractions (closed form). This is the forward implication of abbi , proved from fewer axioms. (Contributed by BJ and WL and SN, 20-Aug-2023)

	Ref	Expression
Assertion	abbi1	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } )

Proof

Step	Hyp	Ref	Expression
1		spsbbi	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜓 ) )
2		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
3		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ↔ [ 𝑦 / 𝑥 ] 𝜓 )
4	1 2 3	3bitr4g	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ 𝜓 } ) )
5	4	eqrdv	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } )