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

Metamath Proof Explorer

Theorem sbbibvv

Description: Reversal of substitution. (Contributed by AV, 6-Aug-2023)

Ref Expression
Assertion sbbibvv ⊢ ∀ y y x φ ↔ ψ ↔ ∀ x φ ↔ x y ψ

Proof

Step Hyp Ref Expression
1 nfv ⊢ Ⅎ y φ
2 nfv ⊢ Ⅎ x ψ
3 1 2 sbbib ⊢ ∀ y y x φ ↔ ψ ↔ ∀ x φ ↔ x y ψ