Theorem sbcex2

Description: Move existential quantifier in and out of class substitution. (Contributed by NM, 21-May-2004) (Revised by NM, 18-Aug-2018)

	Ref	Expression
Assertion	sbcex2	⊢ ( [ 𝐴 / 𝑦 ] ∃ 𝑥 𝜑 ↔ ∃ 𝑥 [ 𝐴 / 𝑦 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sbcex	⊢ ( [ 𝐴 / 𝑦 ] ∃ 𝑥 𝜑 → 𝐴 ∈ V )
2		sbcex	⊢ ( [ 𝐴 / 𝑦 ] 𝜑 → 𝐴 ∈ V )
3	2	exlimiv	⊢ ( ∃ 𝑥 [ 𝐴 / 𝑦 ] 𝜑 → 𝐴 ∈ V )
4		dfsbcq2	⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑦 ] ∃ 𝑥 𝜑 ↔ [ 𝐴 / 𝑦 ] ∃ 𝑥 𝜑 ) )
5		dfsbcq2	⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑦 ] 𝜑 ) )
6	5	exbidv	⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 [ 𝐴 / 𝑦 ] 𝜑 ) )
7		sbex	⊢ ( [ 𝑧 / 𝑦 ] ∃ 𝑥 𝜑 ↔ ∃ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 )
8	4 6 7	vtoclbg	⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑦 ] ∃ 𝑥 𝜑 ↔ ∃ 𝑥 [ 𝐴 / 𝑦 ] 𝜑 ) )
9	1 3 8	pm5.21nii	⊢ ( [ 𝐴 / 𝑦 ] ∃ 𝑥 𝜑 ↔ ∃ 𝑥 [ 𝐴 / 𝑦 ] 𝜑 )