Theorem toponrestid 21790

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 21785	. . . 4 ⊢ 𝐵 = ∪ 𝐴
3	2	restid 16910	. . 3 ⊢ (𝐴 ∈ (TopOn‘𝐵) → (𝐴 ↾t 𝐵) = 𝐴)
4	1, 3	ax-mp 5	. 2 ⊢ (𝐴 ↾t 𝐵) = 𝐴
5	4	eqcomi 2743	1 ⊢ 𝐴 = (𝐴 ↾t 𝐵)

Syntax hints:   = wceq 1543   ∈ wcel 2110  ‘cfv 6369  (class class class)co 7202   ↾_t crest 16897  TopOnctopon 21779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2706  ax-rep 5168  ax-sep 5181  ax-nul 5188  ax-pow 5247  ax-pr 5311  ax-un 7512

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2726  df-clel 2812  df-nfc 2882  df-ne 2936  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3403  df-sbc 3688  df-csb 3803  df-dif 3860  df-un 3862  df-in 3864  df-ss 3874  df-nul 4228  df-if 4430  df-pw 4505  df-sn 4532  df-pr 4534  df-op 4538  df-uni 4810  df-iun 4896  df-br 5044  df-opab 5106  df-mpt 5125  df-id 5444  df-xp 5546  df-rel 5547  df-cnv 5548  df-co 5549  df-dm 5550  df-rn 5551  df-res 5552  df-ima 5553  df-iota 6327  df-fun 6371  df-fn 6372  df-f 6373  df-f1 6374  df-fo 6375  df-f1o 6376  df-fv 6377  df-ov 7205  df-oprab 7206  df-mpo 7207  df-rest 16899  df-topon 21780

This theorem is referenced by:  cncfcn1  23780  cncfmpt2f  23784  cdivcncf  23790  cnrehmeo  23822  cnlimc  24757  dvidlem  24784  dvcnp2  24789  dvcn  24790  dvnres  24800  dvaddbr  24807  dvmulbr  24808  dvcobr  24815  dvcjbr  24818  dvrec  24824  dvexp3  24847  dveflem  24848  dvlipcn  24863  lhop1lem  24882  ftc1cn  24912  dvply1  25149  dvtaylp  25234  taylthlem2  25238  psercn  25290  pserdvlem2  25292  pserdv  25293  abelth  25305  logcn  25507  dvloglem  25508  dvlog  25511  dvlog2  25513  efopnlem2  25517  logtayl  25520  cxpcn  25603  cxpcn2  25604  cxpcn3  25606  resqrtcn  25607  sqrtcn  25608  dvatan  25790  ftalem3  25929  cxpcncf1  32259  knoppcnlem10  34376  knoppcnlem11  34377  dvtan  35521  ftc1cnnc  35543  dvasin  35555  dvacos  35556  cxpcncf2  43069