Metamath Proof Explorer


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 × A dom dom F = A

Proof

Step Hyp Ref Expression
1 fndm F Fn A × A dom F = A × A
2 dmeq dom F = A × A dom dom F = dom A × A
3 dmxpid dom A × A = A
4 2 3 eqtrdi dom F = A × A dom dom F = A
5 1 4 syl F Fn A × A dom dom F = A