Metamath Proof Explorer

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	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
	Assertion	stoweidlem4	$⊢ (φ \land B \in ℝ) \to (t \in T ⟼ B) \in A$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem4.1	$⊢ (φ \land x \in ℝ) \to (t \in T ⟼ x) \in A$
2		eleq1	$⊢ x = B \to (x \in ℝ \leftrightarrow B \in ℝ)$
3	2	anbi2d	$⊢ x = B \to ((φ \land x \in ℝ) \leftrightarrow (φ \land B \in ℝ))$
4		simpl	$⊢ (x = B \land t \in T) \to x = B$
5	4	mpteq2dva	$⊢ x = B \to (t \in T ⟼ x) = (t \in T ⟼ B)$
6	5	eleq1d	$⊢ x = B \to ((t \in T ⟼ x) \in A \leftrightarrow (t \in T ⟼ B) \in A)$
7	3 6	imbi12d	$⊢ x = B \to (((φ \land x \in ℝ) \to (t \in T ⟼ x) \in A) \leftrightarrow ((φ \land B \in ℝ) \to (t \in T ⟼ B) \in A))$
8	7 1	vtoclg	$⊢ B \in ℝ \to ((φ \land B \in ℝ) \to (t \in T ⟼ B) \in A)$
9	8	anabsi7	$⊢ (φ \land B \in ℝ) \to (t \in T ⟼ B) \in A$