Theorem stoweidlem4

Description: Lemma for stoweid : a class variable replaces a setvar variable, for constant functions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypothesis	stoweidlem4.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
Assertion	stoweidlem4	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝐵 ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem4.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
2		eleq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ ℝ ↔ 𝐵 ∈ ℝ ) )
3	2	anbi2d	⊢ ( 𝑥 = 𝐵 → ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ↔ ( 𝜑 ∧ 𝐵 ∈ ℝ ) ) )
4		simpl	⊢ ( ( 𝑥 = 𝐵 ∧ 𝑡 ∈ 𝑇 ) → 𝑥 = 𝐵 )
5	4	mpteq2dva	⊢ ( 𝑥 = 𝐵 → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) = ( 𝑡 ∈ 𝑇 ↦ 𝐵 ) )
6	5	eleq1d	⊢ ( 𝑥 = 𝐵 → ( ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 ↔ ( 𝑡 ∈ 𝑇 ↦ 𝐵 ) ∈ 𝐴 ) )
7	3 6	imbi12d	⊢ ( 𝑥 = 𝐵 → ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝐵 ) ∈ 𝐴 ) ) )
8	7 1	vtoclg	⊢ ( 𝐵 ∈ ℝ → ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝐵 ) ∈ 𝐴 ) )
9	8	anabsi7	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝐵 ) ∈ 𝐴 )