sbex

Description: Move existential quantifier in and out of substitution. (Contributed by NM, 27-Sep-2003)

		Ref	Expression
	Assertion	sbex	$⊢ [z/ y] \exists x φ \leftrightarrow \exists x [z/ y] φ$

Step	Hyp	Ref	Expression
1		sbn	$⊢ [z/ y] \neg \forall x \neg φ \leftrightarrow \neg [z/ y] \forall x \neg φ$
2		sbn	$⊢ [z/ y] \neg φ \leftrightarrow \neg [z/ y] φ$
3	2	sbalv	$⊢ [z/ y] \forall x \neg φ \leftrightarrow \forall x \neg [z/ y] φ$
4	1 3	xchbinx	$⊢ [z/ y] \neg \forall x \neg φ \leftrightarrow \neg \forall x \neg [z/ y] φ$
5		df-ex	$⊢ \exists x φ \leftrightarrow \neg \forall x \neg φ$
6	5	sbbii	$⊢ [z/ y] \exists x φ \leftrightarrow [z/ y] \neg \forall x \neg φ$
7		df-ex	$⊢ \exists x [z/ y] φ \leftrightarrow \neg \forall x \neg [z/ y] φ$
8	4 6 7	3bitr4i	$⊢ [z/ y] \exists x φ \leftrightarrow \exists x [z/ y] φ$

Metamath Proof Explorer