Metamath Proof Explorer

Theorem abbibOLD

Description: Obsolete version of abbib as of 22-Oct-2026. (Contributed by NM, 25-Nov-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion abbibOLD ⊢ 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 φ ↔ ψ