![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dffn4 | Structured version Visualization version GIF version |
Description: A function maps onto its range. (Contributed by NM, 10-May-1998.) |
Ref | Expression |
---|---|
dffn4 | ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2778 | . . 3 ⊢ ran 𝐹 = ran 𝐹 | |
2 | 1 | biantru 522 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹)) |
3 | df-fo 6194 | . 2 ⊢ (𝐹:𝐴–onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹)) | |
4 | 2, 3 | bitr4i 270 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 387 = wceq 1507 ran crn 5408 Fn wfn 6183 –onto→wfo 6186 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-9 2059 ax-ext 2750 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-cleq 2771 df-fo 6194 |
This theorem is referenced by: funforn 6426 fimadmfo 6428 ffoss 7459 tposf2 7719 rneqdmfinf1o 8595 fidomdm 8596 pwfilem 8613 indexfi 8627 intrnfi 8675 fifo 8691 ixpiunwdom 8850 infpwfien 9282 infmap2 9438 cfflb 9479 cfslb2n 9488 ttukeylem6 9734 dmct 9744 fnrndomg 9756 rankcf 9997 tskuni 10003 tskurn 10009 fseqsupcl 13160 vdwlem6 16178 0ram2 16213 0ramcl 16215 quslem 16672 gsumval3 18781 gsumzoppg 18817 mplsubrglem 19933 rncmp 21708 cmpsub 21712 tgcmp 21713 hauscmplem 21718 conncn 21738 2ndcctbss 21767 2ndcomap 21770 2ndcsep 21771 comppfsc 21844 ptcnplem 21933 txtube 21952 txcmplem1 21953 tx1stc 21962 tx2ndc 21963 qtopid 22017 qtopcmplem 22019 qtopkgen 22022 kqtopon 22039 kqopn 22046 kqcld 22047 qtopf1 22128 rnelfm 22265 fmfnfmlem2 22267 fmfnfm 22270 alexsubALT 22363 ptcmplem2 22365 tmdgsum2 22408 tsmsxplem1 22464 met1stc 22834 met2ndci 22835 uniiccdif 23882 dyadmbl 23904 mbfimaopnlem 23959 i1fadd 23999 i1fmul 24000 itg1addlem4 24003 i1fmulc 24007 mbfi1fseqlem4 24022 limciun 24195 aannenlem3 24622 efabl 24835 logccv 24947 locfinreflem 30754 mvrsfpw 32279 msrfo 32319 mtyf 32325 bj-inftyexpitaufo 33959 itg2addnclem2 34391 istotbnd3 34497 sstotbnd 34501 prdsbnd 34519 cntotbnd 34522 heiborlem1 34537 heibor 34547 dihintcl 37931 |
Copyright terms: Public domain | W3C validator |