This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem abbi

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

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

Proof

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