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 ⊢ ∀ x φ ↔ ψ → x | φ = x | ψ

Proof

Step Hyp Ref Expression
1 spsbbi ⊢ ∀ x φ ↔ ψ → y x φ ↔ y x ψ
2 df-clab ⊢ y ∈ x | φ ↔ y x φ
3 df-clab ⊢ y ∈ x | ψ ↔ y x ψ
4 1 2 3 3bitr4g ⊢ ∀ x φ ↔ ψ → y ∈ x | φ ↔ y ∈ x | ψ
5 4 eqrdv ⊢ ∀ x φ ↔ ψ → x | φ = x | ψ