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 e. V -> ( topGen ` B ) = { x | E. y ( y C_ B /\ x = U. y ) } )

Proof

Step	Hyp	Ref	Expression
1		eltg3	|- ( B e. V -> ( x e. ( topGen ` B ) <-> E. y ( y C_ B /\ x = U. y ) ) )
2	1	abbi2dv	|- ( B e. V -> ( topGen ` B ) = { x | E. y ( y C_ B /\ x = U. y ) } )