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

Metamath Proof Explorer

Theorem sbmo

Description: Substitution into an at-most-one quantifier. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion sbmo ( [ 𝑦 / 𝑥 ] ∃* 𝑧 𝜑 ↔ ∃* 𝑧 [ 𝑦 / 𝑥 ] 𝜑 )

Proof

Step Hyp Ref Expression
1 sbex ⊢ ( [ 𝑦 / 𝑥 ] ∃ 𝑤 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑤 ) ↔ ∃ 𝑤 [ 𝑦 / 𝑥 ] ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑤 ) )
2 nfv ⊢ Ⅎ 𝑥 𝑧 = 𝑤
3 2 sblim ⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝑧 = 𝑤 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 → 𝑧 = 𝑤 ) )
4 3 sbalv ⊢ ( [ 𝑦 / 𝑥 ] ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑤 ) ↔ ∀ 𝑧 ( [ 𝑦 / 𝑥 ] 𝜑 → 𝑧 = 𝑤 ) )
5 4 exbii ⊢ ( ∃ 𝑤 [ 𝑦 / 𝑥 ] ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑤 ) ↔ ∃ 𝑤 ∀ 𝑧 ( [ 𝑦 / 𝑥 ] 𝜑 → 𝑧 = 𝑤 ) )
6 1 5 bitri ⊢ ( [ 𝑦 / 𝑥 ] ∃ 𝑤 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑤 ) ↔ ∃ 𝑤 ∀ 𝑧 ( [ 𝑦 / 𝑥 ] 𝜑 → 𝑧 = 𝑤 ) )
7 df-mo ⊢ ( ∃* 𝑧 𝜑 ↔ ∃ 𝑤 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑤 ) )
8 7 sbbii ⊢ ( [ 𝑦 / 𝑥 ] ∃* 𝑧 𝜑 ↔ [ 𝑦 / 𝑥 ] ∃ 𝑤 ∀ 𝑧 ( 𝜑 → 𝑧 = 𝑤 ) )
9 df-mo ⊢ ( ∃* 𝑧 [ 𝑦 / 𝑥 ] 𝜑 ↔ ∃ 𝑤 ∀ 𝑧 ( [ 𝑦 / 𝑥 ] 𝜑 → 𝑧 = 𝑤 ) )
10 6 8 9 3bitr4i ⊢ ( [ 𝑦 / 𝑥 ] ∃* 𝑧 𝜑 ↔ ∃* 𝑧 [ 𝑦 / 𝑥 ] 𝜑 )