Theorem sbcexf

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

	Ref	Expression
Hypothesis	sbcexf.1	⊢ Ⅎ 𝑦 𝐴
Assertion	sbcexf	⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑦 𝜑 ↔ ∃ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sbcexf.1	⊢ Ⅎ 𝑦 𝐴
2		nfv	⊢ Ⅎ 𝑧 𝜑
3	2	sb8ev	⊢ ( ∃ 𝑦 𝜑 ↔ ∃ 𝑧 [ 𝑧 / 𝑦 ] 𝜑 )
4	3	sbcbii	⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑦 𝜑 ↔ [ 𝐴 / 𝑥 ] ∃ 𝑧 [ 𝑧 / 𝑦 ] 𝜑 )
5		sbcex2	⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑧 [ 𝑧 / 𝑦 ] 𝜑 ↔ ∃ 𝑧 [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 )
6		nfs1v	⊢ Ⅎ 𝑦 [ 𝑧 / 𝑦 ] 𝜑
7	1 6	nfsbcw	⊢ Ⅎ 𝑦 [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑
8		nfv	⊢ Ⅎ 𝑧 [ 𝐴 / 𝑥 ] 𝜑
9		sbequ12r	⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑦 ] 𝜑 ↔ 𝜑 ) )
10	9	sbcbidv	⊢ ( 𝑧 = 𝑦 → ( [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
11	7 8 10	cbvexv1	⊢ ( ∃ 𝑧 [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ ∃ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 )
12	4 5 11	3bitri	⊢ ( [ 𝐴 / 𝑥 ] ∃ 𝑦 𝜑 ↔ ∃ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 )