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

Metamath Proof Explorer

Theorem sbcov

Description: A composition law for substitution. Version of sbco with a disjoint variable condition using fewer axioms. (Contributed by NM, 14-May-1993) (Revised by GG, 7-Aug-2023) (Proof shortened by SN, 26-Aug-2025)

Ref Expression
Assertion sbcov ⊢ y x x y φ ↔ y x φ

Proof

Step Hyp Ref Expression
1 sbequ12r ⊢ x = y → x y φ ↔ φ
2 1 sbbiiev ⊢ y x x y φ ↔ y x φ