Metamath Proof Explorer

Theorem abbib

Description: Equal class abstractions require equivalent formulas, and conversely. (Contributed by NM, 25-Nov-2013) (Revised by Mario Carneiro, 11-Aug-2016) Remove dependency on ax-8 and df-clel (by avoiding use of cleqh ). (Revised by BJ, 23-Jun-2019) Reverse the biconditional. (Revised by Wolf Lammen, 23-Feb-2025) (Proof shortened by SN, 22-Oct-2026)

Ref Expression
Assertion abbib ⊢ x | φ = x | ψ ↔ ∀ x φ ↔ ψ

Proof

Step Hyp Ref Expression
1 df-clab ⊢ y ∈ x | φ ↔ y x φ
2 df-clab ⊢ y ∈ x | ψ ↔ y x ψ
3 1 2 bibi12i ⊢ y ∈ x | φ ↔ y ∈ x | ψ ↔ y x φ ↔ y x ψ
4 sbbi ⊢ y x φ ↔ ψ ↔ y x φ ↔ y x ψ
5 3 4 bitr4i ⊢ y ∈ x | φ ↔ y ∈ x | ψ ↔ y x φ ↔ ψ
6 5 albii ⊢ ∀ y y ∈ x | φ ↔ y ∈ x | ψ ↔ ∀ y y x φ ↔ ψ
7 dfcleq ⊢ x | φ = x | ψ ↔ ∀ y y ∈ x | φ ↔ y ∈ x | ψ
8 sb8v ⊢ ∀ x φ ↔ ψ ↔ ∀ y y x φ ↔ ψ
9 6 7 8 3bitr4i ⊢ x | φ = x | ψ ↔ ∀ x φ ↔ ψ