Theorem sbex

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

	Ref	Expression
Assertion	sbex	⊢ ( [ 𝑧 / 𝑦 ] ∃ 𝑥 𝜑 ↔ ∃ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sbn	⊢ ( [ 𝑧 / 𝑦 ] ¬ ∀ 𝑥 ¬ 𝜑 ↔ ¬ [ 𝑧 / 𝑦 ] ∀ 𝑥 ¬ 𝜑 )
2		sbn	⊢ ( [ 𝑧 / 𝑦 ] ¬ 𝜑 ↔ ¬ [ 𝑧 / 𝑦 ] 𝜑 )
3	2	sbalv	⊢ ( [ 𝑧 / 𝑦 ] ∀ 𝑥 ¬ 𝜑 ↔ ∀ 𝑥 ¬ [ 𝑧 / 𝑦 ] 𝜑 )
4	1 3	xchbinx	⊢ ( [ 𝑧 / 𝑦 ] ¬ ∀ 𝑥 ¬ 𝜑 ↔ ¬ ∀ 𝑥 ¬ [ 𝑧 / 𝑦 ] 𝜑 )
5		df-ex	⊢ ( ∃ 𝑥 𝜑 ↔ ¬ ∀ 𝑥 ¬ 𝜑 )
6	5	sbbii	⊢ ( [ 𝑧 / 𝑦 ] ∃ 𝑥 𝜑 ↔ [ 𝑧 / 𝑦 ] ¬ ∀ 𝑥 ¬ 𝜑 )
7		df-ex	⊢ ( ∃ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ↔ ¬ ∀ 𝑥 ¬ [ 𝑧 / 𝑦 ] 𝜑 )
8	4 6 7	3bitr4i	⊢ ( [ 𝑧 / 𝑦 ] ∃ 𝑥 𝜑 ↔ ∃ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 )