Theorem dmxp 5926

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.)

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		df-xp 5681	. . 3 ⊢ (𝐴 × 𝐵) = {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
2	1	dmeqi 5902	. 2 ⊢ dom (𝐴 × 𝐵) = dom {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
3		n0 4345	. . . . 5 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐵)
4	3	biimpi 215	. . . 4 ⊢ (𝐵 ≠ ∅ → ∃𝑥 𝑥 ∈ 𝐵)
5	4	ralrimivw 3150	. . 3 ⊢ (𝐵 ≠ ∅ → ∀𝑦 ∈ 𝐴 ∃𝑥 𝑥 ∈ 𝐵)
6		dmopab3 5917	. . 3 ⊢ (∀𝑦 ∈ 𝐴 ∃𝑥 𝑥 ∈ 𝐵 ↔ dom {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} = 𝐴)
7	5, 6	sylib 217	. 2 ⊢ (𝐵 ≠ ∅ → dom {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} = 𝐴)
8	2, 7	eqtrid 2784	1 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541  ∃wex 1781   ∈ wcel 2106   ≠ wne 2940  ∀wral 3061  ∅c0 4321  {copab 5209   × cxp 5673  dom cdm 5675

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-dm 5685

This theorem is referenced by:  dmxpid  5927  rnxp  6166  dmxpss  6167  ssxpb  6170  relrelss  6269  unixp  6278  xpexr2  7906  xpexcnv  7907  frxp  8108  mpocurryd  8250  fodomr  9124  nqerf  10921  dmtrclfv  14961  pwsbas  17429  pwsle  17434  imasaddfnlem  17470  imasvscafn  17479  efgrcl  19577  frlmip  21324  txindislem  23128  metustexhalf  24056  rrxip  24898  dveq0  25508  dv11cn  25509  noxp1o  27155  noextendseq  27159  bdayfo  27169  noetasuplem2  27226  noetasuplem4  27228  noetainflem2  27230  noetainflem4  27232  mbfmcst  33246  eulerpartlemt  33358  0rrv  33438  curf  36454  curunc  36458  ismgmOLD  36706  diophrw  41482  onnog  42165  onnobdayg  42166  bdaybndbday  42168