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) Definitial form. (Revised by Wolf Lammen, 23-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 dfcleq ⊢ x | φ = x | ψ ↔ ∀ y y ∈ x | φ ↔ y ∈ x | ψ
2 nfsab1 ⊢ Ⅎ x y ∈ x | φ
3 nfsab1 ⊢ Ⅎ x y ∈ x | ψ
4 2 3 nfbi ⊢ Ⅎ x y ∈ x | φ ↔ y ∈ x | ψ
5 nfv ⊢ Ⅎ y φ ↔ ψ
6 df-clab ⊢ y ∈ x | φ ↔ y x φ
7 sbequ12r ⊢ y = x → y x φ ↔ φ
8 6 7 bitrid ⊢ y = x → y ∈ x | φ ↔ φ
9 df-clab ⊢ y ∈ x | ψ ↔ y x ψ
10 sbequ12r ⊢ y = x → y x ψ ↔ ψ
11 9 10 bitrid ⊢ y = x → y ∈ x | ψ ↔ ψ
12 8 11 bibi12d ⊢ y = x → y ∈ x | φ ↔ y ∈ x | ψ ↔ φ ↔ ψ
13 4 5 12 cbvalv1 ⊢ ∀ y y ∈ x | φ ↔ y ∈ x | ψ ↔ ∀ x φ ↔ ψ
14 1 13 bitri ⊢ x | φ = x | ψ ↔ ∀ x φ ↔ ψ