Theorem elpredg

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

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

Proof

Step	Hyp	Ref	Expression
1		df-pred	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
2	1	elin2	⊢ ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑌 ∈ 𝐴 ∧ 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ) )
3	2	baib	⊢ ( 𝑌 ∈ 𝐴 → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ) )
4	3	adantl	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ) )
5		elimasng	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ ◡ 𝑅 ) )
6		df-br	⊢ ( 𝑋 ◡ 𝑅 𝑌 ↔ ⟨ 𝑋 , 𝑌 ⟩ ∈ ◡ 𝑅 )
7	5 6	bitr4di	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ ( ◡ 𝑅 “ { 𝑋 } ) ↔ 𝑋 ◡ 𝑅 𝑌 ) )
8		brcnvg	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 ◡ 𝑅 𝑌 ↔ 𝑌 𝑅 𝑋 ) )
9	4 7 8	3bitrd	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ 𝑌 𝑅 𝑋 ) )