Metamath Proof Explorer


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 ( ( 𝐴𝐵 ∧ ∀ 𝑥𝐵 𝜑 ) → [ 𝐴 / 𝑥 ] 𝜑 )