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 2821 | . . 3 ⊢ ran 𝐹 = ran 𝐹 | |
2 | 1 | biantru 532 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹)) |
3 | df-fo 6361 | . 2 ⊢ (𝐹:𝐴–onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹)) | |
4 | 2, 3 | bitr4i 280 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∧ wa 398 = wceq 1537 ran crn 5556 Fn wfn 6350 –onto→wfo 6353 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-9 2124 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-cleq 2814 df-fo 6361 |
This theorem is referenced by: funforn 6597 fimadmfo 6599 ffoss 7647 tposf2 7916 rneqdmfinf1o 8800 fidomdm 8801 pwfilem 8818 indexfi 8832 intrnfi 8880 fifo 8896 ixpiunwdom 9055 infpwfien 9488 infmap2 9640 cfflb 9681 cfslb2n 9690 ttukeylem6 9936 dmct 9946 fnrndomg 9958 rankcf 10199 tskuni 10205 tskurn 10211 fseqsupcl 13346 vdwlem6 16322 0ram2 16357 0ramcl 16359 quslem 16816 gsumval3 19027 gsumzoppg 19064 mplsubrglem 20219 rncmp 22004 cmpsub 22008 tgcmp 22009 hauscmplem 22014 conncn 22034 2ndcctbss 22063 2ndcomap 22066 2ndcsep 22067 comppfsc 22140 ptcnplem 22229 txtube 22248 txcmplem1 22249 tx1stc 22258 tx2ndc 22259 qtopid 22313 qtopcmplem 22315 qtopkgen 22318 kqtopon 22335 kqopn 22342 kqcld 22343 qtopf1 22424 rnelfm 22561 fmfnfmlem2 22563 fmfnfm 22566 alexsubALT 22659 ptcmplem2 22661 tmdgsum2 22704 tsmsxplem1 22761 met1stc 23131 met2ndci 23132 uniiccdif 24179 dyadmbl 24201 mbfimaopnlem 24256 i1fadd 24296 i1fmul 24297 itg1addlem4 24300 i1fmulc 24304 mbfi1fseqlem4 24319 limciun 24492 aannenlem3 24919 efabl 25134 logccv 25246 locfinreflem 31104 mvrsfpw 32753 msrfo 32793 mtyf 32799 bj-inftyexpitaufo 34487 itg2addnclem2 34959 istotbnd3 35064 sstotbnd 35068 prdsbnd 35086 cntotbnd 35089 heiborlem1 35104 heibor 35114 dihintcl 38495 |
Copyright terms: Public domain | W3C validator |