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	$$⊢FFn\left(A\times A\right)\to \mathrm{dom}\mathrm{dom}F=A$$

Proof

Step	Hyp	Ref	Expression
1		fndm	$$⊢FFn\left(A\times A\right)\to \mathrm{dom}F=A\times A$$
2		dmeq	$$⊢\mathrm{dom}F=A\times A\to \mathrm{dom}\mathrm{dom}F=\mathrm{dom}\left(A\times A\right)$$
3		dmxpid	$$⊢\mathrm{dom}\left(A\times A\right)=A$$
4	2 3	eqtrdi	$$⊢\mathrm{dom}F=A\times A\to \mathrm{dom}\mathrm{dom}F=A$$
5	1 4	syl	$$⊢FFn\left(A\times A\right)\to \mathrm{dom}\mathrm{dom}F=A$$