Theorem predel

Description: Membership in the predecessor class implies membership in the base class. (Contributed by Scott Fenton, 11-Feb-2011)

	Ref	Expression
Assertion	predel	⊢ ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → 𝑌 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elinel1	⊢ ( 𝑌 ∈ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) → 𝑌 ∈ 𝐴 )
2		df-pred	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
3	1 2	eleq2s	⊢ ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → 𝑌 ∈ 𝐴 )