Theorem toponrestid 22643

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

Syntax hints:   = wceq 1539   ∈ wcel 2104  ‘cfv 6542  (class class class)co 7411   ↾_t crest 17370  TopOnctopon 22632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-rest 17372  df-topon 22633

This theorem is referenced by:  cncfcn1  24651  cncfmpt2f  24655  cdivcncf  24661  cnrehmeo  24698  cnrehmeoOLD  24699  mulcncf  25194  cnlimc  25637  dvidlem  25664  dvcnp2  25669  dvcnp2OLD  25670  dvcn  25671  dvnres  25681  dvaddbr  25688  dvmulbr  25689  dvmulbrOLD  25690  dvcobr  25697  dvcobrOLD  25698  dvcjbr  25701  dvrec  25707  dvexp3  25730  dveflem  25731  dvlipcn  25746  lhop1lem  25765  ftc1cn  25795  dvply1  26033  dvtaylp  26118  taylthlem2  26122  psercn  26174  pserdvlem2  26176  pserdv  26177  abelth  26189  logcn  26391  dvloglem  26392  dvlog  26395  dvlog2  26397  efopnlem2  26401  logtayl  26404  cxpcn  26489  cxpcn2  26490  cxpcn3  26492  resqrtcn  26493  sqrtcn  26494  dvatan  26676  ftalem3  26815  cxpcncf1  33905  gg-cxpcn  35470  knoppcnlem10  35681  knoppcnlem11  35682  dvtan  36841  ftc1cnnc  36863  dvasin  36875  dvacos  36876  cxpcncf2  44913