Theorem sbcexfi

Description: Move existential quantifier in and out of class substitution, with an explicit nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 30-May-2019)

	Ref	Expression
Hypotheses	sbcexfi.1	⊢ Ⅎ 𝑦 𝐴
	sbcexfi.2	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜓 )
Assertion	sbcexfi	⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑦 𝜑 ↔ ∃ 𝑦 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		sbcexfi.1	⊢ Ⅎ 𝑦 𝐴
2		sbcexfi.2	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜓 )
3	1	sbcexf	⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑦 𝜑 ↔ ∃ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 )
4	2	exbii	⊢ ( ∃ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 ↔ ∃ 𝑦 𝜓 )
5	3 4	bitri	⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑦 𝜑 ↔ ∃ 𝑦 𝜓 )