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	|- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
Assertion	stoweidlem4	|- ( ( ph /\ B e. RR ) -> ( t e. T |-> B ) e. A )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem4.1	|- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
2		eleq1	|- ( x = B -> ( x e. RR <-> B e. RR ) )
3	2	anbi2d	|- ( x = B -> ( ( ph /\ x e. RR ) <-> ( ph /\ B e. RR ) ) )
4		simpl	|- ( ( x = B /\ t e. T ) -> x = B )
5	4	mpteq2dva	|- ( x = B -> ( t e. T |-> x ) = ( t e. T |-> B ) )
6	5	eleq1d	|- ( x = B -> ( ( t e. T |-> x ) e. A <-> ( t e. T |-> B ) e. A ) )
7	3 6	imbi12d	|- ( x = B -> ( ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A ) <-> ( ( ph /\ B e. RR ) -> ( t e. T |-> B ) e. A ) ) )
8	7 1	vtoclg	|- ( B e. RR -> ( ( ph /\ B e. RR ) -> ( t e. T |-> B ) e. A ) )
9	8	anabsi7	|- ( ( ph /\ B e. RR ) -> ( t e. T |-> B ) e. A )