Theorem dfateq12d

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

	Ref	Expression
Hypotheses	dfateq12d.1	|- ( ph -> F = G )
	dfateq12d.2	|- ( ph -> A = B )
Assertion	dfateq12d	|- ( ph -> ( F defAt A <-> G defAt B ) )

Proof

Step	Hyp	Ref	Expression
1		dfateq12d.1	|- ( ph -> F = G )
2		dfateq12d.2	|- ( ph -> A = B )
3	1	dmeqd	|- ( ph -> dom F = dom G )
4	2 3	eleq12d	|- ( ph -> ( A e. dom F <-> B e. dom G ) )
5	2	sneqd	|- ( ph -> { A } = { B } )
6	1 5	reseq12d	|- ( ph -> ( F |` { A } ) = ( G |` { B } ) )
7	6	funeqd	|- ( ph -> ( Fun ( F |` { A } ) <-> Fun ( G |` { B } ) ) )
8	4 7	anbi12d	|- ( ph -> ( ( A e. dom F /\ Fun ( F |` { A } ) ) <-> ( B e. dom G /\ Fun ( G |` { B } ) ) ) )
9		df-dfat	|- ( F defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) )
10		df-dfat	|- ( G defAt B <-> ( B e. dom G /\ Fun ( G |` { B } ) ) )
11	8 9 10	3bitr4g	|- ( ph -> ( F defAt A <-> G defAt B ) )