Theorem elpred

Description: Membership in a predecessor class. (Contributed by Scott Fenton, 4-Feb-2011)

	Ref	Expression
Hypothesis	elpred.1	⊢ 𝑌 ∈ V
Assertion	elpred	⊢ ( 𝑋 ∈ 𝐷 → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑌 ∈ 𝐴 ∧ 𝑌 𝑅 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elpred.1	⊢ 𝑌 ∈ V
2		df-pred	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
3	2	elin2	⊢ ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ) )
4	1	eliniseg	⊢ ( 𝑋 ∈ 𝐷 → ( 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ↔ 𝑌 𝑅 𝑋 ) )
5	4	anbi2d	⊢ ( 𝑋 ∈ 𝐷 → ( ( 𝑌 ∈ 𝐴 ∧ 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ) ↔ ( 𝑌 ∈ 𝐴 ∧ 𝑌 𝑅 𝑋 ) ) )
6	3 5	syl5bb	⊢ ( 𝑋 ∈ 𝐷 → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑌 ∈ 𝐴 ∧ 𝑌 𝑅 𝑋 ) ) )