sbmo

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

		Ref	Expression
	Assertion	sbmo	$⊢ [y/ x] \exists^{} z φ \leftrightarrow \exists^{} z [y/ x] φ$

Step	Hyp	Ref	Expression
1		sbex	$⊢ [y/ x] \exists w \forall z (φ \to z = w) \leftrightarrow \exists w [y/ x] \forall z (φ \to z = w)$
2		nfv	$⊢ Ⅎ x z = w$
3	2	sblim	$⊢ [y/ x] (φ \to z = w) \leftrightarrow ([y/ x] φ \to z = w)$
4	3	sbalv	$⊢ [y/ x] \forall z (φ \to z = w) \leftrightarrow \forall z ([y/ x] φ \to z = w)$
5	4	exbii	$⊢ \exists w [y/ x] \forall z (φ \to z = w) \leftrightarrow \exists w \forall z ([y/ x] φ \to z = w)$
6	1 5	bitri	$⊢ [y/ x] \exists w \forall z (φ \to z = w) \leftrightarrow \exists w \forall z ([y/ x] φ \to z = w)$
7		df-mo	$⊢ \exists^{*} z φ \leftrightarrow \exists w \forall z (φ \to z = w)$
8	7	sbbii	$⊢ [y/ x] \exists^{*} z φ \leftrightarrow [y/ x] \exists w \forall z (φ \to z = w)$
9		df-mo	$⊢ \exists^{*} z [y/ x] φ \leftrightarrow \exists w \forall z ([y/ x] φ \to z = w)$
10	6 8 9	3bitr4i	$⊢ [y/ x] \exists^{} z φ \leftrightarrow \exists^{} z [y/ x] φ$

Metamath Proof Explorer