Theorem dmxp 5953

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 2141, ax-11 2158, ax-12 2178. (Revised by SN, 12-Aug-2025.)

Assertion

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

Proof of Theorem dmxp

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3492	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm 5925	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 × 𝐵) ↔ ∃𝑦 𝑥(𝐴 × 𝐵)𝑦)
3		brxp 5749	. . . . 5 ⊢ (𝑥(𝐴 × 𝐵)𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
4	3	exbii 1846	. . . 4 ⊢ (∃𝑦 𝑥(𝐴 × 𝐵)𝑦 ↔ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5		19.42v 1953	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵))
6	2, 4, 5	3bitri 297	. . 3 ⊢ (𝑥 ∈ dom (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵))
7		n0 4376	. . . . 5 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐵)
8	7	biimpi 216	. . . 4 ⊢ (𝐵 ≠ ∅ → ∃𝑦 𝑦 ∈ 𝐵)
9	8	biantrud 531	. . 3 ⊢ (𝐵 ≠ ∅ → (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵)))
10	6, 9	bitr4id 290	. 2 ⊢ (𝐵 ≠ ∅ → (𝑥 ∈ dom (𝐴 × 𝐵) ↔ 𝑥 ∈ 𝐴))
11	10	eqrdv 2738	1 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537  ∃wex 1777   ∈ wcel 2108   ≠ wne 2946  ∅c0 4352   class class class wbr 5166   × cxp 5698  dom cdm 5700

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-dm 5710

This theorem is referenced by:  dmxpid  5955  rnxp  6201  dmxpss  6202  ssxpb  6205  relrelss  6304  unixp  6313  xpexr2  7959  xpexcnv  7960  frxp  8167  mpocurryd  8310  fodomr  9194  fodomfir  9396  nqerf  10999  dmtrclfv  15067  pwsbas  17547  pwsle  17552  imasaddfnlem  17588  imasvscafn  17597  efgrcl  19757  frlmip  21821  txindislem  23662  metustexhalf  24590  rrxip  25443  dveq0  26059  dv11cn  26060  noxp1o  27726  noextendseq  27730  bdayfo  27740  noetasuplem2  27797  noetasuplem4  27799  noetainflem2  27801  noetainflem4  27803  mbfmcst  34224  eulerpartlemt  34336  0rrv  34416  curf  37558  curunc  37562  ismgmOLD  37810  diophrw  42715  onnog  43391  onnobdayg  43392  bdaybndbday  43394