Theorem elpredg

Description: Membership in a predecessor class. (Contributed by Scott Fenton, 17-Apr-2011) (Proof shortened by BJ, 16-Oct-2024)

	Ref	Expression
Assertion	elpredg	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ 𝑌 𝑅 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		elpredgg	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑌 ∈ 𝐴 ∧ 𝑌 𝑅 𝑋 ) ) )
2		ibar	⊢ ( 𝑌 ∈ 𝐴 → ( 𝑌 𝑅 𝑋 ↔ ( 𝑌 ∈ 𝐴 ∧ 𝑌 𝑅 𝑋 ) ) )
3	2	bicomd	⊢ ( 𝑌 ∈ 𝐴 → ( ( 𝑌 ∈ 𝐴 ∧ 𝑌 𝑅 𝑋 ) ↔ 𝑌 𝑅 𝑋 ) )
4	3	adantl	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝑌 ∈ 𝐴 ∧ 𝑌 𝑅 𝑋 ) ↔ 𝑌 𝑅 𝑋 ) )
5	1 4	bitrd	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ 𝑌 𝑅 𝑋 ) )