This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbbib

Description: Reversal of substitution. (Contributed by AV, 6-Aug-2023) (Proof shortened by Wolf Lammen, 4-Sep-2023)

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

Proof

Step Hyp Ref Expression
1 sbbib.y ⊢ Ⅎ y φ
2 sbbib.x ⊢ Ⅎ x ψ
3 nfs1v ⊢ Ⅎ x y x φ
4 3 2 nfbi ⊢ Ⅎ x y x φ ↔ ψ
5 nfs1v ⊢ Ⅎ y x y ψ
6 1 5 nfbi ⊢ Ⅎ y φ ↔ x y ψ
7 sbequ12r ⊢ y = x → y x φ ↔ φ
8 sbequ12 ⊢ y = x → ψ ↔ x y ψ
9 7 8 bibi12d ⊢ y = x → y x φ ↔ ψ ↔ φ ↔ x y ψ
10 4 6 9 cbvalv1 ⊢ ∀ y y x φ ↔ ψ ↔ ∀ x φ ↔ x y ψ