| 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 6849 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴) | |
| 2 | fndm 6671 | . 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 dom cdm 5685 Fn wfn 6556 –1-1-onto→wf1o 6560 |
| 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 207 df-an 396 df-fn 6564 df-f 6565 df-f1 6566 df-f1o 6568 |
| This theorem is referenced by: f1imacnv 6864 f1ounsn 7292 f1opw2 7688 xpcomco 9102 domss2 9176 mapen 9181 ssenen 9191 phplem2 9245 php3 9249 phplem4OLD 9257 php3OLD 9261 f1opwfi 9396 unxpwdom2 9628 cnfcomlem 9739 djuun 9966 ackbij2lem2 10279 ackbij2lem3 10280 fin4en1 10349 enfin2i 10361 gsumpropd2lem 18692 symgfixf1 19455 f1omvdmvd 19461 f1omvdconj 19464 pmtrfb 19483 symggen 19488 symggen2 19489 psgnunilem1 19511 basqtop 23719 reghmph 23801 nrmhmph 23802 indishmph 23806 ordthmeolem 23809 ufldom 23970 tgpconncompeqg 24120 imasf1oxms 24502 icchmeo 24971 icchmeoOLD 24972 dvcvx 26059 dvloglem 26690 f1ocnt 32804 cycpmconjvlem 33161 cycpmconjslem2 33175 madjusmdetlem2 33827 madjusmdetlem4 33829 tpr2rico 33911 ballotlemrv 34522 reprpmtf1o 34641 hgt750lemg 34669 subfacp1lem2b 35186 subfacp1lem5 35189 poimirlem3 37630 ismtyres 37815 eldioph2lem1 42771 lnmlmic 43100 ntrclsiex 44066 ntrneiiex 44089 ssnnf1octb 45199 f1oresf1o 47302 grimuhgr 47878 isubgr3stgrlem3 47935 |
| Copyright terms: Public domain | W3C validator |