Theorem resexg 3401

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 2724	. 2 |- (A e. C -> (A i^i (B X. V)) e. V)
2		df-res 3197	. 2 |- (A |` B) = (A i^i (B X. V))
3	1, 2	syl5eqel 1555	1 |- (A e. C -> (A |` B) e. V)

Syntax hints:   -> wi 3   e. wcel 960  Vcvv 1814   i^i cin 2050   X. cxp 3175   |` cres 3179

This theorem is referenced by:  mapunen 4509  php3 4522  php3OLD 4523  ssfi 4549  ssfiOLD 4550  fodomfi 4582  fodomfiOLD 4583  seq1res 6335  seq0fval 6543  seqzfval 6545  seqzresval 6567  seqzres 6568  dfseq0 6571  climres 7112  clim2serz 7152  ruclem5 7522  metreslem 7826  hhssva 9131  hhsssm 9132  hhssnm 9133  hhshsslem1 9139  hhsssh2 9142

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2709

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-in 2055  df-res 3197

Copyright terms: Public domain