Theorem dmxp 5878

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 2147, ax-11 2163, ax-12 2185. (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 3434	. . . . 5 ⊢ 𝑥 ∈ V
2	1	eldm 5849	. . . 4 ⊢ (𝑥 ∈ dom (𝐴 × 𝐵) ↔ ∃𝑦 𝑥(𝐴 × 𝐵)𝑦)
3		brxp 5673	. . . . 5 ⊢ (𝑥(𝐴 × 𝐵)𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
4	3	exbii 1850	. . . 4 ⊢ (∃𝑦 𝑥(𝐴 × 𝐵)𝑦 ↔ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5		19.42v 1955	. . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵))
6	2, 4, 5	3bitri 297	. . 3 ⊢ (𝑥 ∈ dom (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵))
7		n0 4294	. . . . 5 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐵)
8	7	biimpi 216	. . . 4 ⊢ (𝐵 ≠ ∅ → ∃𝑦 𝑦 ∈ 𝐵)
9	8	biantrud 531	. . 3 ⊢ (𝐵 ≠ ∅ → (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵)))
10	6, 9	bitr4id 290	. 2 ⊢ (𝐵 ≠ ∅ → (𝑥 ∈ dom (𝐴 × 𝐵) ↔ 𝑥 ∈ 𝐴))
11	10	eqrdv 2735	1 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ≠ wne 2933  ∅c0 4274   class class class wbr 5086   × cxp 5622  dom cdm 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5630  df-dm 5634

This theorem is referenced by:  dmxpid  5879  rnxp  6128  dmxpss  6129  ssxpb  6132  relrelss  6231  unixp  6240  xpexr2  7863  xpexcnv  7864  frxp  8069  mpocurryd  8212  fodomr  9059  fodomfir  9231  nqerf  10844  dmtrclfv  14971  pwsbas  17441  pwsle  17447  imasaddfnlem  17483  imasvscafn  17492  efgrcl  19681  frlmip  21768  txindislem  23608  metustexhalf  24531  rrxip  25367  dveq0  25977  dv11cn  25978  noxp1o  27641  noextendseq  27645  bdayfo  27655  noetasuplem2  27712  noetasuplem4  27714  noetainflem2  27716  noetainflem4  27718  dmdju  32735  fxpgaval  33243  mbfmcst  34419  eulerpartlemt  34531  0rrv  34611  curf  37933  curunc  37937  ismgmOLD  38185  diophrw  43205  onnoxpg  43874  onnobdayg  43875  bdaybndbday  43877  dmrnxp  49324