Metamath Proof Explorer

Theorem sbalOLD

Description: Obsolete version of sbal as of 13-Aug-2023. Move universal quantifier in and out of substitution. (Contributed by NM, 16-May-1993) (Proof shortened by Wolf Lammen, 29-Sep-2018) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion sbalOLD ⊢ z y ∀ x φ ↔ ∀ x z y φ

Proof

Step Hyp Ref Expression
1 nfae ⊢ Ⅎ y ∀ x x = z
2 axc16gb ⊢ ∀ x x = z → φ ↔ ∀ x φ
3 1 2 sbbid ⊢ ∀ x x = z → z y φ ↔ z y ∀ x φ
4 axc16gb ⊢ ∀ x x = z → z y φ ↔ ∀ x z y φ
5 3 4 bitr3d ⊢ ∀ x x = z → z y ∀ x φ ↔ ∀ x z y φ
6 sbal1 ⊢ ¬ ∀ x x = z → z y ∀ x φ ↔ ∀ x z y φ
7 5 6 pm2.61i ⊢ z y ∀ x φ ↔ ∀ x z y φ