Metamath Proof Explorer


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 BVtopGenB=x|yyBx=y

Proof

Step Hyp Ref Expression
1 eltg3 BVxtopGenByyBx=y
2 1 abbi2dv BVtopGenB=x|yyBx=y