Theorem rspesbcd

Description: Restricted quantifier version of spesbcd . (Contributed by Eric Schmidt, 29-Sep-2025)

	Ref	Expression
Hypotheses	rspesbcd.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	rspesbcd.2	⊢ ( 𝜑 → [ 𝐴 / 𝑥 ] 𝜓 )
Assertion	rspesbcd	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		rspesbcd.1	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
2		rspesbcd.2	⊢ ( 𝜑 → [ 𝐴 / 𝑥 ] 𝜓 )
3		sbcel1v	⊢ ( [ 𝐴 / 𝑥 ] 𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 )
4	1 3	sylibr	⊢ ( 𝜑 → [ 𝐴 / 𝑥 ] 𝑥 ∈ 𝐵 )
5		sbcan	⊢ ( [ 𝐴 / 𝑥 ] ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑥 ∈ 𝐵 ∧ [ 𝐴 / 𝑥 ] 𝜓 ) )
6	4 2 5	sylanbrc	⊢ ( 𝜑 → [ 𝐴 / 𝑥 ] ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) )
7	6	spesbcd	⊢ ( 𝜑 → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) )
8		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐵 𝜓 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜓 ) )
9	7 8	sylibr	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐵 𝜓 )