Theorem restid 15332

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 6588	. . 3 |- ( J e. V -> U. J e. _V )
3	1, 2	syl5eqel 2533	. 2 |- ( J e. V -> X e. _V )
4	1	eqimss2i 3487	. . 3 |- U. J C_ X
5		sspwuni 4367	. . 3 |- ( J C_ ~P X <-> U. J C_ X )
6	4, 5	mpbir 213	. 2 |- J C_ ~P X
7		restid2 15329	. 2 |- ( ( X e. _V /\ J C_ ~P X ) -> ( J ↾t X ) = J )
8	3, 6, 7	sylancl 668	1 |- ( J e. V -> ( J ↾t X ) = J )

Syntax hints:   -> wi 4   = wceq 1444   e. wcel 1887   _Vcvv 3045   C_ wss 3404   ~Pcpw 3951   U.cuni 4198  (class class class)co 6290   ↾_t crest 15319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-rest 15321

This theorem is referenced by:  restin  20182  cnrmnrm  20377  cmpkgen  20566  xkopt  20670  xkoinjcn  20702  ussid  21275  tuslem  21282  cnperf  21838  retopcon  21847  cncfcn1  21942  cncfmpt2f  21946  cdivcncf  21949  abscncfALT  21952  cnmpt2pc  21956  cnrehmeo  21981  cnlimc  22843  recnperf  22860  dvidlem  22870  dvcnp2  22874  dvcn  22875  dvnres  22885  dvaddbr  22892  dvmulbr  22893  dvcobr  22900  dvcjbr  22903  dvrec  22909  dvexp3  22930  dveflem  22931  dvlipcn  22946  lhop1lem  22965  ftc1cn  22995  dvply1  23237  dvtaylp  23325  taylthlem2  23329  psercn  23381  pserdvlem2  23383  pserdv  23384  abelth  23396  logcn  23592  dvloglem  23593  dvlog  23596  dvlog2  23598  efopnlem2  23602  logtayl  23605  cxpcn  23685  cxpcn2  23686  cxpcn3  23688  resqrtcn  23689  sqrtcn  23690  dvatan  23861  ftalem3  23999  retopscon  29972  ivthALT  30991  dvtan  31992  ftc1cnnc  32016  dvasin  32028  dvacos  32029  binomcxplemdvbinom  36702  binomcxplemnotnn0  36705  fsumcncf  37755  ioccncflimc  37763  cncfuni  37764  icocncflimc  37767  cncfiooicclem1  37771  cxpcncf2  37778  itgsubsticclem  37852  dirkercncflem2  37966  dirkercncflem4  37968  fourierdlem32  38002  fourierdlem33  38003  fourierdlem62  38032  fourierdlem93  38063  fourierdlem101  38071