Metamath Proof Explorer


Theorem sb8mo

Description: Variable substitution for the at-most-one quantifier. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Alexander van der Vekens, 17-Jun-2017) (New usage is discouraged.)

Ref Expression
Hypothesis sb8eu.1 y φ
Assertion sb8mo * x φ * y y x φ

Proof

Step Hyp Ref Expression
1 sb8eu.1 y φ
2 1 sb8e x φ y y x φ
3 1 sb8eu ∃! x φ ∃! y y x φ
4 2 3 imbi12i x φ ∃! x φ y y x φ ∃! y y x φ
5 moeu * x φ x φ ∃! x φ
6 moeu * y y x φ y y x φ ∃! y y x φ
7 4 5 6 3bitr4i * x φ * y y x φ