This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbcth2

Description: A substitution into a theorem. (Contributed by NM, 1-Mar-2008) (Proof shortened by Mario Carneiro, 13-Oct-2016)

Ref Expression
Hypothesis sbcth2.1 ⊢ ( 𝑥 ∈ 𝐵 → 𝜑 )
Assertion sbcth2 ( 𝐴 ∈ 𝐵 → [ 𝐴 / 𝑥 ] 𝜑 )

Proof

Step Hyp Ref Expression
1 sbcth2.1 ⊢ ( 𝑥 ∈ 𝐵 → 𝜑 )
2 1 rgen ⊢ ∀ 𝑥 ∈ 𝐵 𝜑
3 rspsbc ⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 𝜑 → [ 𝐴 / 𝑥 ] 𝜑 ) )
4 2 3 mpi ⊢ ( 𝐴 ∈ 𝐵 → [ 𝐴 / 𝑥 ] 𝜑 )