Theorem resss

Description: A class includes its restriction. Exercise 15 of TakeutiZaring p. 25. (Contributed by NM, 2-Aug-1994)

	Ref	Expression
Assertion	resss	⊢ ( 𝐴 ↾ 𝐵 ) ⊆ 𝐴

Proof

Step	Hyp	Ref	Expression
1		df-res	⊢ ( 𝐴 ↾ 𝐵 ) = ( 𝐴 ∩ ( 𝐵 × V ) )
2		inss1	⊢ ( 𝐴 ∩ ( 𝐵 × V ) ) ⊆ 𝐴
3	1 2	eqsstri	⊢ ( 𝐴 ↾ 𝐵 ) ⊆ 𝐴