![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1odm | Structured version Visualization version Unicode version |
Description: The domain of a one-to-one onto mapping. (Contributed by NM, 8-Mar-2014.) |
Ref | Expression |
---|---|
f1odm |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1ofn 5837 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | fndm 5696 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 17 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
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 190 df-an 377 df-fn 5603 df-f 5604 df-f1 5605 df-f1o 5607 |
This theorem is referenced by: f1imacnv 5852 f1opw2 6548 xpcomco 7687 domss2 7756 mapen 7761 ssenen 7771 phplem4 7779 php3 7783 f1opwfi 7903 unxpwdom2 8128 cnfcomlem 8229 ackbij2lem2 8695 ackbij2lem3 8696 fin4en1 8764 enfin2i 8776 hashfacen 12649 gsumpropd2lem 16564 symgbas 17069 symgfixf1 17126 f1omvdmvd 17132 f1omvdconj 17135 pmtrfb 17154 symggen 17159 symggen2 17160 psgnunilem1 17182 basqtop 20774 reghmph 20856 nrmhmph 20857 indishmph 20861 ordthmeolem 20864 ufldom 21025 tgpconcompeqg 21174 imasf1oxms 21552 icchmeo 22017 dvcvx 23020 dvloglem 23641 f1ocnt 28424 madjusmdetlem2 28702 madjusmdetlem4 28704 tpr2rico 28766 ballotlemrv 29400 ballotlemrvOLD 29438 subfacp1lem2b 29952 subfacp1lem5 29955 poimirlem3 31987 ismtyres 32184 eldioph2lem1 35646 lnmlmic 35990 ssnnf1octb 37507 |
Copyright terms: Public domain | W3C validator |