Theorem toponrestid 22806

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  ‘cfv 6482  (class class class)co 7349   ↾_t crest 17324  TopOnctopon 22795

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-oprab 7353  df-mpo 7354  df-rest 17326  df-topon 22796

This theorem is referenced by:  cncfcn1  24802  cncfmpt2f  24806  cdivcncf  24812  cnrehmeo  24849  cnrehmeoOLD  24850  mulcncf  25344  cnlimc  25787  dvidlem  25814  dvcnp2  25819  dvcnp2OLD  25820  dvcn  25821  dvnres  25831  dvaddbr  25838  dvmulbr  25839  dvmulbrOLD  25840  dvcobr  25847  dvcobrOLD  25848  dvcjbr  25851  dvrec  25857  dvexp3  25880  dveflem  25881  dvlipcn  25897  lhop1lem  25916  ftc1cn  25948  dvply1  26189  dvtaylp  26276  taylthlem2  26280  taylthlem2OLD  26281  psercn  26334  pserdvlem2  26336  pserdv  26337  abelth  26349  logcn  26554  dvloglem  26555  dvlog  26558  dvlog2  26560  efopnlem2  26564  logtayl  26567  cxpcn  26652  cxpcnOLD  26653  cxpcn2  26654  cxpcn3  26656  resqrtcn  26657  sqrtcn  26658  dvatan  26843  ftalem3  26983  cxpcncf1  34563  knoppcnlem10  36476  knoppcnlem11  36477  dvtan  37650  ftc1cnnc  37672  dvasin  37684  dvacos  37685  cxpcncf2  45880