Theorem restid 14364

Description: The subspace topology of the base set is the original topology. (Contributed by Jeff Hankins, 9-Jul-2009.) (Revised by Mario Carneiro, 13-Aug-2015.)

Hypothesis

Ref	Expression
restid.1	|- X = U. J

Assertion

Ref	Expression
restid	|- ( J e. V -> ( J ↾t X ) = J )

Proof of Theorem restid

Step	Hyp	Ref	Expression
1		restid.1	. . 3 |- X = U. J
2		uniexg 6372	. . 3 |- ( J e. V -> U. J e. _V )
3	1, 2	syl5eqel 2522	. 2 |- ( J e. V -> X e. _V )
4	1	eqimss2i 3406	. . 3 |- U. J C_ X
5		sspwuni 4251	. . 3 |- ( J C_ ~P X <-> U. J C_ X )
6	4, 5	mpbir 209	. 2 |- J C_ ~P X
7		restid2 14361	. 2 |- ( ( X e. _V /\ J C_ ~P X ) -> ( J ↾t X ) = J )
8	3, 6, 7	sylancl 662	1 |- ( J e. V -> ( J ↾t X ) = J )

Syntax hints:   -> wi 4   = wceq 1369   e. wcel 1756   _Vcvv 2967   C_ wss 3323   ~Pcpw 3855   U.cuni 4086  (class class class)co 6086   ↾_t crest 14351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-rest 14353

This theorem is referenced by:  restin  18745  cnrmnrm  18940  cmpkgen  19099  xkopt  19203  xkoinjcn  19235  ussid  19810  tuslem  19817  cnperf  20372  retopcon  20381  cncfcn1  20461  cncfmpt2f  20465  cdivcncf  20468  abscncfALT  20471  cnmpt2pc  20475  cnrehmeo  20500  cnlimc  21338  recnperf  21355  dvidlem  21365  dvcnp2  21369  dvcn  21370  dvnres  21380  dvaddbr  21387  dvmulbr  21388  dvcobr  21395  dvcjbr  21398  dvrec  21404  dvexp3  21425  dveflem  21426  dvlipcn  21441  lhop1lem  21460  ftc1cn  21490  dvply1  21725  dvtaylp  21810  taylthlem2  21814  psercn  21866  pserdvlem2  21868  pserdv  21869  abelth  21881  logcn  22067  dvloglem  22068  dvlog  22071  dvlog2  22073  efopnlem2  22077  logtayl  22080  cxpcn  22158  cxpcn2  22159  cxpcn3  22161  resqrcn  22162  sqrcn  22163  dvatan  22305  ftalem3  22387  retopscon  27090  dvtan  28395  ftc1cnnc  28419  dvasin  28433  dvacos  28434  ivthALT  28483