MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmxp Structured version   Visualization version   GIF version

Theorem dmxp 5938
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 2140, ax-11 2156, ax-12 2176. (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.
StepHypRef Expression
1 vex 3483 . . . . 5 𝑥 ∈ V
21eldm 5910 . . . 4 (𝑥 ∈ dom (𝐴 × 𝐵) ↔ ∃𝑦 𝑥(𝐴 × 𝐵)𝑦)
3 brxp 5733 . . . . 5 (𝑥(𝐴 × 𝐵)𝑦 ↔ (𝑥𝐴𝑦𝐵))
43exbii 1847 . . . 4 (∃𝑦 𝑥(𝐴 × 𝐵)𝑦 ↔ ∃𝑦(𝑥𝐴𝑦𝐵))
5 19.42v 1952 . . . 4 (∃𝑦(𝑥𝐴𝑦𝐵) ↔ (𝑥𝐴 ∧ ∃𝑦 𝑦𝐵))
62, 4, 53bitri 297 . . 3 (𝑥 ∈ dom (𝐴 × 𝐵) ↔ (𝑥𝐴 ∧ ∃𝑦 𝑦𝐵))
7 n0 4352 . . . . 5 (𝐵 ≠ ∅ ↔ ∃𝑦 𝑦𝐵)
87biimpi 216 . . . 4 (𝐵 ≠ ∅ → ∃𝑦 𝑦𝐵)
98biantrud 531 . . 3 (𝐵 ≠ ∅ → (𝑥𝐴 ↔ (𝑥𝐴 ∧ ∃𝑦 𝑦𝐵)))
106, 9bitr4id 290 . 2 (𝐵 ≠ ∅ → (𝑥 ∈ dom (𝐴 × 𝐵) ↔ 𝑥𝐴))
1110eqrdv 2734 1 (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1539  wex 1778  wcel 2107  wne 2939  c0 4332   class class class wbr 5142   × cxp 5682  dom cdm 5684
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143  df-opab 5205  df-xp 5690  df-dm 5694
This theorem is referenced by:  dmxpid  5940  rnxp  6189  dmxpss  6190  ssxpb  6193  relrelss  6292  unixp  6301  xpexr2  7942  xpexcnv  7943  frxp  8152  mpocurryd  8295  fodomr  9169  fodomfir  9369  nqerf  10971  dmtrclfv  15058  pwsbas  17533  pwsle  17538  imasaddfnlem  17574  imasvscafn  17583  efgrcl  19734  frlmip  21799  txindislem  23642  metustexhalf  24570  rrxip  25425  dveq0  26040  dv11cn  26041  noxp1o  27709  noextendseq  27713  bdayfo  27723  noetasuplem2  27780  noetasuplem4  27782  noetainflem2  27784  noetainflem4  27786  dmdju  32658  mbfmcst  34262  eulerpartlemt  34374  0rrv  34454  curf  37606  curunc  37610  ismgmOLD  37858  diophrw  42775  onnog  43447  onnobdayg  43448  bdaybndbday  43450
  Copyright terms: Public domain W3C validator