Theorem fnxpdmdm

Description: The domain of the domain of a function over a Cartesian square. (Contributed by AV, 13-Jan-2020)

	Ref	Expression
Assertion	fnxpdmdm	|- ( F Fn ( A X. A ) -> dom dom F = A )

Proof

Step	Hyp	Ref	Expression
1		fndm	|- ( F Fn ( A X. A ) -> dom F = ( A X. A ) )
2		dmeq	|- ( dom F = ( A X. A ) -> dom dom F = dom ( A X. A ) )
3		dmxpid	|- dom ( A X. A ) = A
4	2 3	eqtrdi	|- ( dom F = ( A X. A ) -> dom dom F = A )
5	1 4	syl	|- ( F Fn ( A X. A ) -> dom dom F = A )