Theorem bnj1418

Description: Property of _pred . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Assertion	bnj1418	⊢ ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → 𝑦 𝑅 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		breq1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 𝑅 𝑥 ↔ 𝑦 𝑅 𝑥 ) )
2		df-bnj14	⊢ pred ( 𝑥 , 𝐴 , 𝑅 ) = { 𝑧 ∈ 𝐴 ∣ 𝑧 𝑅 𝑥 }
3	2	bnj1538	⊢ ( 𝑧 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → 𝑧 𝑅 𝑥 )
4	1 3	vtoclga	⊢ ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → 𝑦 𝑅 𝑥 )