Metamath Proof Explorer


Theorem dmdju

Description: Domain of a disjoint union of non-empty sets. (Contributed by Thierry Arnoux, 5-Oct-2025)

Ref Expression
Hypothesis dmdju.1 φ x A B
Assertion dmdju φ dom x A x × B = A

Proof

Step Hyp Ref Expression
1 dmdju.1 φ x A B
2 dmiun dom x A x × B = x A dom x × B
3 dmxp B dom x × B = x
4 1 3 syl φ x A dom x × B = x
5 4 iuneq2dv φ x A dom x × B = x A x
6 2 5 eqtrid φ dom x A x × B = x A x
7 iunid x A x = A
8 6 7 eqtrdi φ dom x A x × B = A