![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dmxp | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
dmxp | ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3481 | . . . . 5 ⊢ 𝑥 ∈ V | |
2 | 1 | eldm 5913 | . . . 4 ⊢ (𝑥 ∈ dom (𝐴 × 𝐵) ↔ ∃𝑦 𝑥(𝐴 × 𝐵)𝑦) |
3 | brxp 5737 | . . . . 5 ⊢ (𝑥(𝐴 × 𝐵)𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | |
4 | 3 | exbii 1844 | . . . 4 ⊢ (∃𝑦 𝑥(𝐴 × 𝐵)𝑦 ↔ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
5 | 19.42v 1950 | . . . 4 ⊢ (∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵)) | |
6 | 2, 4, 5 | 3bitri 297 | . . 3 ⊢ (𝑥 ∈ dom (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵)) |
7 | n0 4358 | . . . . 5 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝐵) | |
8 | 7 | biimpi 216 | . . . 4 ⊢ (𝐵 ≠ ∅ → ∃𝑦 𝑦 ∈ 𝐵) |
9 | 8 | biantrud 531 | . . 3 ⊢ (𝐵 ≠ ∅ → (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐵))) |
10 | 6, 9 | bitr4id 290 | . 2 ⊢ (𝐵 ≠ ∅ → (𝑥 ∈ dom (𝐴 × 𝐵) ↔ 𝑥 ∈ 𝐴)) |
11 | 10 | eqrdv 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 |