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 6662 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴) | |
2 | fndm 6481 | . 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 dom cdm 5551 Fn wfn 6375 –1-1-onto→wf1o 6379 |
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 210 df-an 400 df-fn 6383 df-f 6384 df-f1 6385 df-f1o 6387 |
This theorem is referenced by: f1imacnv 6677 f1opw2 7460 xpcomco 8735 domss2 8805 mapen 8810 ssenen 8820 phplem4 8828 php3 8832 f1opwfi 8980 unxpwdom2 9204 cnfcomlem 9314 djuun 9542 ackbij2lem2 9854 ackbij2lem3 9855 fin4en1 9923 enfin2i 9935 hashfacenOLD 14019 gsumpropd2lem 18151 symgfixf1 18829 f1omvdmvd 18835 f1omvdconj 18838 pmtrfb 18857 symggen 18862 symggen2 18863 psgnunilem1 18885 basqtop 22608 reghmph 22690 nrmhmph 22691 indishmph 22695 ordthmeolem 22698 ufldom 22859 tgpconncompeqg 23009 imasf1oxms 23387 icchmeo 23838 dvcvx 24917 dvloglem 25536 f1ocnt 30843 cycpmconjvlem 31127 cycpmconjslem2 31141 madjusmdetlem2 31492 madjusmdetlem4 31494 tpr2rico 31576 ballotlemrv 32198 reprpmtf1o 32318 hgt750lemg 32346 subfacp1lem2b 32856 subfacp1lem5 32859 poimirlem3 35517 ismtyres 35703 eldioph2lem1 40285 lnmlmic 40616 ntrclsiex 41340 ntrneiiex 41363 ssnnf1octb 42406 f1oresf1o 44454 |
Copyright terms: Public domain | W3C validator |