Theorem tgval3

Description: Alternate expression for the topology generated by a basis. Lemma 2.1 of Munkres p. 80. See also tgval and tgval2 . (Contributed by NM, 17-Jul-2006) (Revised by Mario Carneiro, 30-Aug-2015)

	Ref	Expression
Assertion	tgval3	$$⊢B\in V\to \mathrm{topGen}\left(B\right)=\left\{x|\exists y\left(y\subseteq B\wedge x=\bigcup y\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		eltg3	$$⊢B\in V\to \left(x\in \mathrm{topGen}\left(B\right)\leftrightarrow \exists y\left(y\subseteq B\wedge x=\bigcup y\right)\right)$$
2	1	eqabdv	$$⊢B\in V\to \mathrm{topGen}\left(B\right)=\left\{x|\exists y\left(y\subseteq B\wedge x=\bigcup y\right)\right\}$$