Theorem resexg 3394

Description: The restriction of a set is a set.

Assertion

Ref	Expression
resexg	|- (A e. C -> (A |` B) e. V)

Proof of Theorem resexg

Step	Hyp	Ref	Expression
1		inex1g 2718	. 2 |- (A e. C -> (A i^i (B X. V)) e. V)
2		df-res 3190	. 2 |- (A |` B) = (A i^i (B X. V))
3	1, 2	syl5eqel 1552	1 |- (A e. C -> (A |` B) e. V)

Syntax hints:   -> wi 3   e. wcel 958  Vcvv 1811   i^i cin 2046   X. cxp 3168   |` cres 3172

This theorem is referenced by:  mapunen 4502  php3 4515  php3OLD 4516  ssfi 4537  ssfiOLD 4538  fodomfiOLD 4566  seq1res 6327  seq0fval 6535  seqzfval 6537  seqzresval 6559  seqzres 6560  dfseq0 6563  climres 7105  clim2serz 7145  ruclem5 7514  metreslem 7822  hhssva 9129  hhsssm 9130  hhssnm 9131  hhshsslem1 9137  hhsssh2 9140

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-in 2051  df-res 3190

Copyright terms: Public domain