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 2610 | . . 3 ⊢ ran 𝐹 = ran 𝐹 | |
2 | 1 | biantru 525 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹)) |
3 | df-fo 5810 | . 2 ⊢ (𝐹:𝐴–onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹)) | |
4 | 2, 3 | bitr4i 266 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ wa 383 = wceq 1475 ran crn 5039 Fn wfn 5799 –onto→wfo 5802 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-an 385 df-cleq 2603 df-fo 5810 |
This theorem is referenced by: funforn 6035 ffoss 7020 tposf2 7263 mapsn 7785 rneqdmfinf1o 8127 fidomdm 8128 pwfilem 8143 indexfi 8157 intrnfi 8205 fifo 8221 ixpiunwdom 8379 infpwfien 8768 infmap2 8923 cfflb 8964 cfslb2n 8973 ttukeylem6 9219 fnrndomg 9239 rankcf 9478 tskuni 9484 tskurn 9490 fseqsupcl 12638 vdwlem6 15528 0ram2 15563 0ramcl 15565 quslem 16026 gsumval3 18131 gsumzoppg 18167 mplsubrglem 19260 rncmp 21009 cmpsub 21013 tgcmp 21014 hauscmplem 21019 concn 21039 2ndcctbss 21068 2ndcomap 21071 2ndcsep 21072 comppfsc 21145 ptcnplem 21234 txtube 21253 txcmplem1 21254 tx1stc 21263 tx2ndc 21264 qtopid 21318 qtopcmplem 21320 qtopkgen 21323 kqtopon 21340 kqopn 21347 kqcld 21348 qtopf1 21429 rnelfm 21567 fmfnfmlem2 21569 fmfnfm 21572 alexsubALT 21665 ptcmplem2 21667 tmdgsum2 21710 tsmsxplem1 21766 met1stc 22136 met2ndci 22137 uniiccdif 23152 dyadmbl 23174 mbfimaopnlem 23228 i1fadd 23268 i1fmul 23269 itg1addlem4 23272 i1fmulc 23276 mbfi1fseqlem4 23291 limciun 23464 aannenlem3 23889 efabl 24100 logccv 24209 dmct 28877 locfinreflem 29235 mvrsfpw 30657 msrfo 30697 mtyf 30703 itg2addnclem2 32632 istotbnd3 32740 sstotbnd 32744 prdsbnd 32762 cntotbnd 32765 heiborlem1 32780 heibor 32790 dihintcl 35651 mapsnd 38383 |
Copyright terms: Public domain | W3C validator |