Metamath Proof Explorer

Theorem abbi

Description: Equivalent formulas define equal class abstractions, 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)

Ref Expression
Assertion abbi ⊢ ∀ 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 syl5bb ⊢ y = x → y ∈ x | φ ↔ φ
9 df-clab ⊢ y ∈ x | ψ ↔ y x ψ
10 sbequ12r ⊢ y = x → y x ψ ↔ ψ
11 9 10 syl5bb ⊢ 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 bitr2i ⊢ ∀ x φ ↔ ψ ↔ x | φ = x | ψ