![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1odm | Structured version Visualization version GIF version |
Description: The domain of a one-to-one onto mapping. (Contributed by NM, 8-Mar-2014.) |
Ref | Expression |
---|---|
f1odm | ⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1ofn 6279 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴) | |
2 | fndm 6130 | . 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1631 dom cdm 5249 Fn wfn 6026 –1-1-onto→wf1o 6030 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 383 df-fn 6034 df-f 6035 df-f1 6036 df-f1o 6038 |
This theorem is referenced by: f1imacnv 6294 f1opw2 7035 xpcomco 8206 domss2 8275 mapen 8280 ssenen 8290 phplem4 8298 php3 8302 f1opwfi 8426 unxpwdom2 8649 cnfcomlem 8760 djuun 8952 ackbij2lem2 9264 ackbij2lem3 9265 fin4en1 9333 enfin2i 9345 hashfacen 13440 gsumpropd2lem 17481 symgbas 18007 symgfixf1 18064 f1omvdmvd 18070 f1omvdconj 18073 pmtrfb 18092 symggen 18097 symggen2 18098 psgnunilem1 18120 basqtop 21735 reghmph 21817 nrmhmph 21818 indishmph 21822 ordthmeolem 21825 ufldom 21986 tgpconncompeqg 22135 imasf1oxms 22514 icchmeo 22960 dvcvx 24003 dvloglem 24615 f1ocnt 29899 madjusmdetlem2 30234 madjusmdetlem4 30236 tpr2rico 30298 ballotlemrv 30921 reprpmtf1o 31044 hgt750lemg 31072 subfacp1lem2b 31501 subfacp1lem5 31504 poimirlem3 33745 ismtyres 33939 eldioph2lem1 37849 lnmlmic 38184 ntrclsiex 38877 ntrneiiex 38900 ssnnf1octb 39902 f1oresf1o 41832 f1oresf1o2 41833 |
Copyright terms: Public domain | W3C validator |