Metamath Proof Explorer

Theorem sbbibOLD

Description: Obsolete version of sbbib as of 4-Sep-2023. (Contributed by AV, 6-Aug-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses sbbibOLD.y ⊢ Ⅎ y φ
sbbibOLD.x ⊢ Ⅎ x ψ
Assertion sbbibOLD ⊢ ∀ y y x φ ↔ ψ ↔ ∀ x φ ↔ x y ψ

Proof

Step Hyp Ref Expression
1 sbbibOLD.y ⊢ Ⅎ y φ
2 sbbibOLD.x ⊢ Ⅎ x ψ
3 nfs1v ⊢ Ⅎ x y x φ
4 3 2 nfbi ⊢ Ⅎ x y x φ ↔ ψ
5 4 nf5ri ⊢ y x φ ↔ ψ → ∀ x y x φ ↔ ψ
6 5 hbal ⊢ ∀ y y x φ ↔ ψ → ∀ x ∀ y y x φ ↔ ψ
7 sbcov ⊢ x y y x φ ↔ x y φ
8 1 sbf ⊢ x y φ ↔ φ
9 7 8 bitri ⊢ x y y x φ ↔ φ
10 spsbbi ⊢ ∀ y y x φ ↔ ψ → x y y x φ ↔ x y ψ
11 9 10 syl5bbr ⊢ ∀ y y x φ ↔ ψ → φ ↔ x y ψ
12 6 11 alrimih ⊢ ∀ y y x φ ↔ ψ → ∀ x φ ↔ x y ψ
13 nfs1v ⊢ Ⅎ y x y ψ
14 1 13 nfbi ⊢ Ⅎ y φ ↔ x y ψ
15 14 nf5ri ⊢ φ ↔ x y ψ → ∀ y φ ↔ x y ψ
16 15 hbal ⊢ ∀ x φ ↔ x y ψ → ∀ y ∀ x φ ↔ x y ψ
17 spsbbi ⊢ ∀ x φ ↔ x y ψ → y x φ ↔ y x x y ψ
18 sbcov ⊢ y x x y ψ ↔ y x ψ
19 2 sbf ⊢ y x ψ ↔ ψ
20 18 19 bitri ⊢ y x x y ψ ↔ ψ
21 17 20 syl6bb ⊢ ∀ x φ ↔ x y ψ → y x φ ↔ ψ
22 16 21 alrimih ⊢ ∀ x φ ↔ x y ψ → ∀ y y x φ ↔ ψ
23 12 22 impbii ⊢ ∀ y y x φ ↔ ψ ↔ ∀ x φ ↔ x y ψ