Theorem dmxp

Description: The domain of a Cartesian product. Part of Theorem 3.13(x) of Monk1 p. 37. (Contributed by NM, 28-Jul-1995) (Proof shortened by Andrew Salmon, 27-Aug-2011) Avoid ax-10 , ax-11 , ax-12 . (Revised by SN, 12-Aug-2025)

	Ref	Expression
Assertion	dmxp	⊢ ( 𝐵 ≠ ∅ → dom ( 𝐴 × 𝐵 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2	1	eldm	⊢ ( 𝑥 ∈ dom ( 𝐴 × 𝐵 ) ↔ ∃ 𝑦 𝑥 ( 𝐴 × 𝐵 ) 𝑦 )
3		brxp	⊢ ( 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
4	3	exbii	⊢ ( ∃ 𝑦 𝑥 ( 𝐴 × 𝐵 ) 𝑦 ↔ ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
5		19.42v	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 ∈ 𝐵 ) )
6	2 4 5	3bitri	⊢ ( 𝑥 ∈ dom ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 ∈ 𝐵 ) )
7		n0	⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐵 )
8	7	biimpi	⊢ ( 𝐵 ≠ ∅ → ∃ 𝑦 𝑦 ∈ 𝐵 )
9	8	biantrud	⊢ ( 𝐵 ≠ ∅ → ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 ∈ 𝐵 ) ) )
10	6 9	bitr4id	⊢ ( 𝐵 ≠ ∅ → ( 𝑥 ∈ dom ( 𝐴 × 𝐵 ) ↔ 𝑥 ∈ 𝐴 ) )
11	10	eqrdv	⊢ ( 𝐵 ≠ ∅ → dom ( 𝐴 × 𝐵 ) = 𝐴 )