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 ] ph <-> [ y / x ] ph )

Proof

Step Hyp Ref Expression
1 sbequ12r
 |-  ( x = y -> ( [ x / y ] ph <-> ph ) )
2 1 sbbiiev
 |-  ( [ y / x ] [ x / y ] ph <-> [ y / x ] ph )