Metamath Proof Explorer

Theorem iscnrm3lem1

Description: Lemma for iscnrm3 . Subspace topology is a topology. (Contributed by Zhi Wang, 3-Sep-2024)

		Ref	Expression
	Assertion	iscnrm3lem1	$⊢ J \in Top \to (\forall x \in A φ \leftrightarrow \forall x \in A (J ↾_{𝑡} x \in Top \land φ))$

Step	Hyp	Ref	Expression
1		resttop	$⊢ (J \in Top \land x \in A) \to J ↾_{𝑡} x \in Top$
2	1	biantrurd	$⊢ (J \in Top \land x \in A) \to (φ \leftrightarrow (J ↾_{𝑡} x \in Top \land φ))$
3	2	ralbidva	$⊢ J \in Top \to (\forall x \in A φ \leftrightarrow \forall x \in A (J ↾_{𝑡} x \in Top \land φ))$