Metamath Proof Explorer


Theorem toponrestid

Description: Given a topology on a set, restricting it to that same set has no effect. (Contributed by Jim Kingdon, 6-Jul-2022)

Ref Expression
Hypothesis toponrestid.t ATopOnB
Assertion toponrestid A=A𝑡B

Proof

Step Hyp Ref Expression
1 toponrestid.t ATopOnB
2 1 toponunii B=A
3 2 restid ATopOnBA𝑡B=A
4 1 3 ax-mp A𝑡B=A
5 4 eqcomi A=A𝑡B