Theorem dmxp 5686

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 5454	. . 3 ⊢ (𝐴 × 𝐵) = {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
2	1	dmeqi 5664	. 2 ⊢ dom (𝐴 × 𝐵) = dom {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
3		n0 4234	. . . . 5 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐵)
4	3	biimpi 217	. . . 4 ⊢ (𝐵 ≠ ∅ → ∃𝑥 𝑥 ∈ 𝐵)
5	4	ralrimivw 3150	. . 3 ⊢ (𝐵 ≠ ∅ → ∀𝑦 ∈ 𝐴 ∃𝑥 𝑥 ∈ 𝐵)
6		dmopab3 5679	. . 3 ⊢ (∀𝑦 ∈ 𝐴 ∃𝑥 𝑥 ∈ 𝐵 ↔ dom {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} = 𝐴)
7	5, 6	sylib 219	. 2 ⊢ (𝐵 ≠ ∅ → dom {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} = 𝐴)
8	2, 7	syl5eq 2843	1 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1522  ∃wex 1761   ∈ wcel 2081   ≠ wne 2984  ∀wral 3105  ∅c0 4215  {copab 5028   × cxp 5446  dom cdm 5448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099  ax-nul 5106  ax-pr 5226

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rab 3114  df-v 3439  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-sn 4477  df-pr 4479  df-op 4483  df-br 4967  df-opab 5029  df-xp 5454  df-dm 5458

This theorem is referenced by:  dmxpid  5687  rnxp  5908  dmxpss  5909  ssxpb  5912  relrelss  6004  unixp  6013  xpexr2  7485  xpexcnv  7486  frxp  7678  mpocurryd  7791  fodomr  8520  nqerf  10203  dmtrclfv  14217  pwsbas  16594  pwsle  16599  imasaddfnlem  16635  imasvscafn  16644  efgrcl  18573  frlmip  20609  txindislem  21930  metustexhalf  22854  rrxip  23681  dveq0  24285  dv11cn  24286  mbfmcst  31139  eulerpartlemt  31251  0rrv  31331  noxp1o  32786  noextendseq  32790  bdayfo  32798  noetalem3  32835  noetalem4  32836  curf  34427  curunc  34431  ismgmOLD  34686  diophrw  38867