Metamath Proof Explorer

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 x φ ψ x | φ = x | ψ


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 | ψ