Theorem bnj602

Description: Equality theorem for the _pred function constant. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Assertion	bnj602	⊢ ( 𝑋 = 𝑌 → pred ( 𝑋 , 𝐴 , 𝑅 ) = pred ( 𝑌 , 𝐴 , 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑋 = 𝑌 → ( 𝑦 𝑅 𝑋 ↔ 𝑦 𝑅 𝑌 ) )
2	1	rabbidv	⊢ ( 𝑋 = 𝑌 → { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑋 } = { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑌 } )
3		df-bnj14	⊢ pred ( 𝑋 , 𝐴 , 𝑅 ) = { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑋 }
4		df-bnj14	⊢ pred ( 𝑌 , 𝐴 , 𝑅 ) = { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑌 }
5	2 3 4	3eqtr4g	⊢ ( 𝑋 = 𝑌 → pred ( 𝑋 , 𝐴 , 𝑅 ) = pred ( 𝑌 , 𝐴 , 𝑅 ) )