Metamath Proof Explorer

Theorem dmdm

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

Ref Expression
Assertion dmdm 
|- ( A Fn ( B X. B ) -> B = dom dom A )

Proof

Step Hyp Ref Expression
1 fndm 
 |-  ( A Fn ( B X. B ) -> dom A = ( B X. B ) )
2 1 dmeqd 
 |-  ( A Fn ( B X. B ) -> dom dom A = dom ( B X. B ) )
3 dmxpid 
 |-  dom ( B X. B ) = B
4 2 3 eqtr2di 
 |-  ( A Fn ( B X. B ) -> B = dom dom A )