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 ( ( 𝜑𝑥𝐴 ) → 𝐵 ≠ ∅ )
Assertion dmdju ( 𝜑 → dom 𝑥𝐴 ( { 𝑥 } × 𝐵 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 dmdju.1 ( ( 𝜑𝑥𝐴 ) → 𝐵 ≠ ∅ )
2 dmiun dom 𝑥𝐴 ( { 𝑥 } × 𝐵 ) = 𝑥𝐴 dom ( { 𝑥 } × 𝐵 )
3 dmxp ( 𝐵 ≠ ∅ → dom ( { 𝑥 } × 𝐵 ) = { 𝑥 } )
4 1 3 syl ( ( 𝜑𝑥𝐴 ) → dom ( { 𝑥 } × 𝐵 ) = { 𝑥 } )
5 4 iuneq2dv ( 𝜑 𝑥𝐴 dom ( { 𝑥 } × 𝐵 ) = 𝑥𝐴 { 𝑥 } )
6 2 5 eqtrid ( 𝜑 → dom 𝑥𝐴 ( { 𝑥 } × 𝐵 ) = 𝑥𝐴 { 𝑥 } )
7 iunid 𝑥𝐴 { 𝑥 } = 𝐴
8 6 7 eqtrdi ( 𝜑 → dom 𝑥𝐴 ( { 𝑥 } × 𝐵 ) = 𝐴 )