This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝐴 × 𝐵 ) = 𝐴 )