Theorem sbcth 2959

Description: A substitution into a theorem remains true (when 𝐴 is a set). (Contributed by NM, 5-Nov-2005.)

Hypothesis

Ref	Expression
sbcth.1	⊢ 𝜑

Assertion

Ref	Expression
sbcth	⊢ (𝐴 ∈ 𝑉 → [𝐴 / 𝑥]𝜑)

Proof of Theorem sbcth

Step	Hyp	Ref	Expression
1		sbcth.1	. . 3 ⊢ 𝜑
2	1	ax-gen 1436	. 2 ⊢ ∀𝑥𝜑
3		spsbc 2957	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥𝜑 → [𝐴 / 𝑥]𝜑))
4	2, 3	mpi 15	1 ⊢ (𝐴 ∈ 𝑉 → [𝐴 / 𝑥]𝜑)

Syntax hints:   → wi 4  ∀wal 1340   ∈ wcel 2135  [wsbc 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-v 2723  df-sbc 2947

This theorem is referenced by:  rabrsndc  3638  iota4an  5166