Theorem dmdm

Description: The double domain of a function on a Cartesian square. (Contributed by Zhi Wang, 1-Nov-2025)

	Ref	Expression
Assertion	dmdm	$$⊢AFn\left(B\times B\right)\to B=\mathrm{dom}\mathrm{dom}A$$

Proof

Step	Hyp	Ref	Expression
1		fndm	$$⊢AFn\left(B\times B\right)\to \mathrm{dom}A=B\times B$$
2	1	dmeqd	$$⊢AFn\left(B\times B\right)\to \mathrm{dom}\mathrm{dom}A=\mathrm{dom}\left(B\times B\right)$$
3		dmxpid	$$⊢\mathrm{dom}\left(B\times B\right)=B$$
4	2 3	eqtr2di	$$⊢AFn\left(B\times B\right)\to B=\mathrm{dom}\mathrm{dom}A$$