Theorem dfateq12d

Description: Equality deduction for "defined at". (Contributed by Alexander van der Vekens, 26-May-2017)

	Ref	Expression
Hypotheses	dfateq12d.1	⊢ ( 𝜑 → 𝐹 = 𝐺 )
	dfateq12d.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
Assertion	dfateq12d	⊢ ( 𝜑 → ( 𝐹 defAt 𝐴 ↔ 𝐺 defAt 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		dfateq12d.1	⊢ ( 𝜑 → 𝐹 = 𝐺 )
2		dfateq12d.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
3	1	dmeqd	⊢ ( 𝜑 → dom 𝐹 = dom 𝐺 )
4	2 3	eleq12d	⊢ ( 𝜑 → ( 𝐴 ∈ dom 𝐹 ↔ 𝐵 ∈ dom 𝐺 ) )
5	2	sneqd	⊢ ( 𝜑 → { 𝐴 } = { 𝐵 } )
6	1 5	reseq12d	⊢ ( 𝜑 → ( 𝐹 ↾ { 𝐴 } ) = ( 𝐺 ↾ { 𝐵 } ) )
7	6	funeqd	⊢ ( 𝜑 → ( Fun ( 𝐹 ↾ { 𝐴 } ) ↔ Fun ( 𝐺 ↾ { 𝐵 } ) ) )
8	4 7	anbi12d	⊢ ( 𝜑 → ( ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ↔ ( 𝐵 ∈ dom 𝐺 ∧ Fun ( 𝐺 ↾ { 𝐵 } ) ) ) )
9		df-dfat	⊢ ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
10		df-dfat	⊢ ( 𝐺 defAt 𝐵 ↔ ( 𝐵 ∈ dom 𝐺 ∧ Fun ( 𝐺 ↾ { 𝐵 } ) ) )
11	8 9 10	3bitr4g	⊢ ( 𝜑 → ( 𝐹 defAt 𝐴 ↔ 𝐺 defAt 𝐵 ) )