Theorem toponrestid 23078

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

Hypothesis

Ref	Expression
toponrestid.t	⊢ 𝐴 ∈ (TopOn‘𝐵)

Assertion

Ref	Expression
toponrestid	⊢ 𝐴 = (𝐴 ↾t 𝐵)

Proof of Theorem toponrestid

Step	Hyp	Ref	Expression
1		toponrestid.t	. . 3 ⊢ 𝐴 ∈ (TopOn‘𝐵)
2	1	toponunii 23073	. . . 4 ⊢ 𝐵 = ∪ 𝐴
3	2	restid 17481	. . 3 ⊢ (𝐴 ∈ (TopOn‘𝐵) → (𝐴 ↾t 𝐵) = 𝐴)
4	1, 3	ax-mp 5	. 2 ⊢ (𝐴 ↾t 𝐵) = 𝐴
5	4	eqcomi 2772	1 ⊢ 𝐴 = (𝐴 ↾t 𝐵)

Syntax hints:   = wceq 1570   ∈ wcel 2143  ‘cfv 6536  (class class class)co 7410   ↾_t crest 17468  TopOnctopon 23067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-rest 17470  df-topon 23068

This theorem is referenced by:  cncfcn1  25070  cncfmpt2f  25074  cdivcncf  25080  cnrehmeo  25112  mulcncf  25605  cnlimc  26047  dvidlem  26074  dvcnp2  26079  dvcn  26080  dvnres  26090  dvaddbr  26097  dvmulbr  26098  dvcobr  26105  dvcjbr  26108  dvrec  26114  dvexp3  26137  dveflem  26138  dvlipcn  26153  lhop1lem  26172  ftc1cn  26202  dvply1  26445  dvtaylp  26533  taylthlem2  26537  psercn  26589  pserdvlem2  26591  pserdv  26592  abelth  26604  logcn  26812  dvloglem  26813  dvlog  26816  dvlog2  26818  efopnlem2  26822  logtayl  26825  cxpcn  26910  cxpcn2  26911  cxpcn3  26913  resqrtcn  26914  sqrtcn  26915  dvatan  27100  ftalem3  27239  cxpcncf1  34982  knoppcnlem10  37091  knoppcnlem11  37092  dvtan  38321  ftc1cnnc  38343  dvasin  38355  dvacos  38356  cxpcncf2  46613