Theorem dmxp 5910

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 2178, ax-11 2194, ax-12 2215. (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 3461	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm 5881	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 × 𝐵) ↔ ∃𝑦 𝑥(𝐴 × 𝐵)𝑦)
3		brxp 5701	. . . . 5 ⊢ (𝑥(𝐴 × 𝐵)𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
4	3	exbii 1871	. . . 4 ⊢ (∃𝑦 𝑥(𝐴 × 𝐵)𝑦 ↔ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5		19.42v 1976	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵))
6	2, 4, 5	3bitri 300	. . 3 ⊢ (𝑥 ∈ dom (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵))
7		n0 4308	. . . . 5 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐵)
8	7	biimpi 219	. . . 4 ⊢ (𝐵 ≠ ∅ → ∃𝑦 𝑦 ∈ 𝐵)
9	8	biantrud 540	. . 3 ⊢ (𝐵 ≠ ∅ → (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵)))
10	6, 9	bitr4id 293	. 2 ⊢ (𝐵 ≠ ∅ → (𝑥 ∈ dom (𝐴 × 𝐵) ↔ 𝑥 ∈ 𝐴))
11	10	eqrdv 2763	1 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563  ∃wex 1802   ∈ wcel 2145   ≠ wne 2960  ∅c0 4288   class class class wbr 5105   × cxp 5650  dom cdm 5652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-xp 5658  df-dm 5662

This theorem is referenced by:  dmxpid  5911  rnxp  6160  dmxpss  6161  ssxpb  6164  relrelss  6264  unixp  6273  xpexr2  7904  xpexcnv  7905  frxp  8110  mpocurryd  8253  fodomr  9104  fodomfir  9275  nqerf  10903  dmtrclfv  15045  pwsbas  17530  pwsle  17536  imasaddfnlem  17572  imasvscafn  17581  efgrcl  19776  frlmip  21888  txindislem  23751  metustexhalf  24674  rrxip  25510  dveq0  26120  dv11cn  26121  noxp1o  27785  noextendseq  27789  bdayfo  27799  noetasuplem2  27856  noetasuplem4  27858  noetainflem2  27860  noetainflem4  27862  dmdju  32904  fxpgaval  33400  mbfmcst  34566  eulerpartlemt  34678  0rrv  34758  curf  38109  curunc  38113  ismgmOLD  38361  diophrw  43352  onnoxpg  44017  onnobdayg  44018  bdaybndbday  44020  dmrnxp  49466