This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝑆 , 𝐵 , 𝑌 ) )