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 𝑦 𝜑
Assertion sb8mo ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )

Proof

Step Hyp Ref Expression
1 sb8eu.1 𝑦 𝜑
2 1 sb8e ( ∃ 𝑥 𝜑 ↔ ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )
3 1 sb8eu ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )
4 2 3 imbi12i ( ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) ↔ ( ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 → ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )
5 moeu ( ∃* 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∃! 𝑥 𝜑 ) )
6 moeu ( ∃* 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ↔ ( ∃ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 → ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )
7 4 5 6 3bitr4i ( ∃* 𝑥 𝜑 ↔ ∃* 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )