Theorem rspsbca

Description: Restricted quantifier version of Axiom 4 of Mendelson p. 69. (Contributed by NM, 14-Dec-2005)

	Ref	Expression
Assertion	rspsbca	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 𝜑 ) → [ 𝐴 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		rspsbc	⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 𝜑 → [ 𝐴 / 𝑥 ] 𝜑 ) )
2	1	imp	⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 𝜑 ) → [ 𝐴 / 𝑥 ] 𝜑 )