![]() |
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.) |
Ref | Expression |
---|---|
dmxp | ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-xp 5640 | . . 3 ⊢ (𝐴 × 𝐵) = {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} | |
2 | 1 | dmeqi 5861 | . 2 ⊢ dom (𝐴 × 𝐵) = dom {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} |
3 | n0 4307 | . . . . 5 ⊢ (𝐵 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐵) | |
4 | 3 | biimpi 215 | . . . 4 ⊢ (𝐵 ≠ ∅ → ∃𝑥 𝑥 ∈ 𝐵) |
5 | 4 | ralrimivw 3144 | . . 3 ⊢ (𝐵 ≠ ∅ → ∀𝑦 ∈ 𝐴 ∃𝑥 𝑥 ∈ 𝐵) |
6 | dmopab3 5876 | . . 3 ⊢ (∀𝑦 ∈ 𝐴 ∃𝑥 𝑥 ∈ 𝐵 ↔ dom {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} = 𝐴) | |
7 | 5, 6 | sylib 217 | . 2 ⊢ (𝐵 ≠ ∅ → dom {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} = 𝐴) |
8 | 2, 7 | eqtrid 2785 | 1 ⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ∃wex 1782 ∈ wcel 2107 ≠ wne 2940 ∀wral 3061 ∅c0 4283 {copab 5168 × cxp 5632 dom cdm 5634 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5257 ax-nul 5264 ax-pr 5385 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2941 df-ral 3062 df-rab 3407 df-v 3446 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-sn 4588 df-pr 4590 df-op 4594 df-br 5107 df-opab 5169 df-xp 5640 df-dm 5644 |
This theorem is referenced by: dmxpid 5886 rnxp 6123 dmxpss 6124 ssxpb 6127 relrelss 6226 unixp 6235 xpexr2 7857 xpexcnv 7858 frxp 8059 mpocurryd 8201 fodomr 9075 nqerf 10871 dmtrclfv 14909 pwsbas 17374 pwsle 17379 imasaddfnlem 17415 imasvscafn 17424 efgrcl 19502 frlmip 21200 txindislem 23000 metustexhalf 23928 rrxip 24770 dveq0 25380 dv11cn 25381 noxp1o 27027 noextendseq 27031 bdayfo 27041 noetasuplem2 27098 noetasuplem4 27100 noetainflem2 27102 noetainflem4 27104 mbfmcst 32916 eulerpartlemt 33028 0rrv 33108 curf 36102 curunc 36106 ismgmOLD 36355 diophrw 41125 onnog 41789 onnobdayg 41790 bdaybndbday 41792 |
Copyright terms: Public domain | W3C validator |