Theorem predss

Description: The predecessor class of A is a subset of A . (Contributed by Scott Fenton, 2-Feb-2011)

	Ref	Expression
Assertion	predss	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐴

Proof

Step	Hyp	Ref	Expression
1		df-pred	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
2		inss1	⊢ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ⊆ 𝐴
3	1 2	eqsstri	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐴