![]() |
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 6476 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴) | |
2 | fndm 6317 | . 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1520 dom cdm 5435 Fn wfn 6212 –1-1-onto→wf1o 6216 |
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 208 df-an 397 df-fn 6220 df-f 6221 df-f1 6222 df-f1o 6224 |
This theorem is referenced by: f1imacnv 6491 f1opw2 7249 xpcomco 8444 domss2 8513 mapen 8518 ssenen 8528 phplem4 8536 php3 8540 f1opwfi 8664 unxpwdom2 8888 cnfcomlem 8997 djuun 9190 ackbij2lem2 9497 ackbij2lem3 9498 fin4en1 9566 enfin2i 9578 hashfacen 13648 gsumpropd2lem 17700 symgbas 18227 symgfixf1 18284 f1omvdmvd 18290 f1omvdconj 18293 pmtrfb 18312 symggen 18317 symggen2 18318 psgnunilem1 18340 basqtop 21991 reghmph 22073 nrmhmph 22074 indishmph 22078 ordthmeolem 22081 ufldom 22242 tgpconncompeqg 22391 imasf1oxms 22770 icchmeo 23216 dvcvx 24288 dvloglem 24900 f1ocnt 30181 cycpmconjvlem 30383 cycpmconjslem2 30393 madjusmdetlem2 30664 madjusmdetlem4 30666 tpr2rico 30728 ballotlemrv 31350 reprpmtf1o 31470 hgt750lemg 31498 subfacp1lem2b 31992 subfacp1lem5 31995 poimirlem3 34372 ismtyres 34564 eldioph2lem1 38792 lnmlmic 39124 ntrclsiex 39839 ntrneiiex 39862 ssnnf1octb 40949 f1oresf1o 42959 |
Copyright terms: Public domain | W3C validator |