Theorem predeq123

Description: Equality theorem for the predecessor class. (Contributed by Scott Fenton, 13-Jun-2018)

	Ref	Expression
Assertion	predeq123	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌 ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( 𝑆 , 𝐵 , 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		simp2	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌 ) → 𝐴 = 𝐵 )
2		cnveq	⊢ ( 𝑅 = 𝑆 → ◡ 𝑅 = ◡ 𝑆 )
3	2	3ad2ant1	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌 ) → ◡ 𝑅 = ◡ 𝑆 )
4		sneq	⊢ ( 𝑋 = 𝑌 → { 𝑋 } = { 𝑌 } )
5	4	3ad2ant3	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌 ) → { 𝑋 } = { 𝑌 } )
6	3 5	imaeq12d	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌 ) → ( ◡ 𝑅 “ { 𝑋 } ) = ( ◡ 𝑆 “ { 𝑌 } ) )
7	1 6	ineq12d	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌 ) → ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐵 ∩ ( ◡ 𝑆 “ { 𝑌 } ) ) )
8		df-pred	⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
9		df-pred	⊢ Pred ( 𝑆 , 𝐵 , 𝑌 ) = ( 𝐵 ∩ ( ◡ 𝑆 “ { 𝑌 } ) )
10	7 8 9	3eqtr4g	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌 ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( 𝑆 , 𝐵 , 𝑌 ) )