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

Theorem dmxp 5941
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 2138, ax-11 2154, ax-12 2174. (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 3481 . . . . 5 𝑥 ∈ V
21eldm 5913 . . . 4 (𝑥 ∈ dom (𝐴 × 𝐵) ↔ ∃𝑦 𝑥(𝐴 × 𝐵)𝑦)
3 brxp 5737 . . . . 5 (𝑥(𝐴 × 𝐵)𝑦 ↔ (𝑥𝐴𝑦𝐵))
43exbii 1844 . . . 4 (∃𝑦 𝑥(𝐴 × 𝐵)𝑦 ↔ ∃𝑦(𝑥𝐴𝑦𝐵))
5 19.42v 1950 . . . 4 (∃𝑦(𝑥𝐴𝑦𝐵) ↔ (𝑥𝐴 ∧ ∃𝑦 𝑦𝐵))
62, 4, 53bitri 297 . . 3 (𝑥 ∈ dom (𝐴 × 𝐵) ↔ (𝑥𝐴 ∧ ∃𝑦 𝑦𝐵))
7 n0 4358 . . . . 5 (𝐵 ≠ ∅ ↔ ∃𝑦 𝑦𝐵)
87biimpi 216 . . . 4 (𝐵 ≠ ∅ → ∃𝑦 𝑦𝐵)
98biantrud 531 . . 3 (𝐵 ≠ ∅ → (𝑥𝐴 ↔ (𝑥𝐴 ∧ ∃𝑦 𝑦𝐵)))
106, 9bitr4id 290 . 2 (𝐵 ≠ ∅ → (𝑥 ∈ dom (𝐴 × 𝐵) ↔ 𝑥𝐴))
1110eqrdv 2732 1 (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1536  wex 1775  wcel 2105  wne 2937  c0 4338   class class class wbr 5147   × cxp 5686  dom cdm 5688
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-dm 5698
This theorem is referenced by:  dmxpid  5943  rnxp  6191  dmxpss  6192  ssxpb  6195  relrelss  6294  unixp  6303  xpexr2  7941  xpexcnv  7942  frxp  8149  mpocurryd  8292  fodomr  9166  fodomfir  9365  nqerf  10967  dmtrclfv  15053  pwsbas  17533  pwsle  17538  imasaddfnlem  17574  imasvscafn  17583  efgrcl  19747  frlmip  21815  txindislem  23656  metustexhalf  24584  rrxip  25437  dveq0  26053  dv11cn  26054  noxp1o  27722  noextendseq  27726  bdayfo  27736  noetasuplem2  27793  noetasuplem4  27795  noetainflem2  27797  noetainflem4  27799  dmdju  32663  mbfmcst  34240  eulerpartlemt  34352  0rrv  34432  curf  37584  curunc  37588  ismgmOLD  37836  diophrw  42746  onnog  43418  onnobdayg  43419  bdaybndbday  43421
  Copyright terms: Public domain W3C validator