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 2622 | . . 3 ⊢ ran 𝐹 = ran 𝐹 | |
2 | 1 | biantru 526 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹)) |
3 | df-fo 5894 | . 2 ⊢ (𝐹:𝐴–onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹)) | |
4 | 2, 3 | bitr4i 267 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 384 = wceq 1483 ran crn 5115 Fn wfn 5883 –onto→wfo 5886 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-cleq 2615 df-fo 5894 |
This theorem is referenced by: funforn 6122 ffoss 7127 tposf2 7376 mapsn 7899 rneqdmfinf1o 8242 fidomdm 8243 pwfilem 8260 indexfi 8274 intrnfi 8322 fifo 8338 ixpiunwdom 8496 infpwfien 8885 infmap2 9040 cfflb 9081 cfslb2n 9090 ttukeylem6 9336 dmct 9346 fnrndomg 9358 rankcf 9599 tskuni 9605 tskurn 9611 fseqsupcl 12776 vdwlem6 15690 0ram2 15725 0ramcl 15727 quslem 16203 gsumval3 18308 gsumzoppg 18344 mplsubrglem 19439 rncmp 21199 cmpsub 21203 tgcmp 21204 hauscmplem 21209 conncn 21229 2ndcctbss 21258 2ndcomap 21261 2ndcsep 21262 comppfsc 21335 ptcnplem 21424 txtube 21443 txcmplem1 21444 tx1stc 21453 tx2ndc 21454 qtopid 21508 qtopcmplem 21510 qtopkgen 21513 kqtopon 21530 kqopn 21537 kqcld 21538 qtopf1 21619 rnelfm 21757 fmfnfmlem2 21759 fmfnfm 21762 alexsubALT 21855 ptcmplem2 21857 tmdgsum2 21900 tsmsxplem1 21956 met1stc 22326 met2ndci 22327 uniiccdif 23346 dyadmbl 23368 mbfimaopnlem 23422 i1fadd 23462 i1fmul 23463 itg1addlem4 23466 i1fmulc 23470 mbfi1fseqlem4 23485 limciun 23658 aannenlem3 24085 efabl 24296 logccv 24409 locfinreflem 29907 mvrsfpw 31403 msrfo 31443 mtyf 31449 itg2addnclem2 33462 istotbnd3 33570 sstotbnd 33574 prdsbnd 33592 cntotbnd 33595 heiborlem1 33610 heibor 33620 dihintcl 36633 mapsnd 39388 |
Copyright terms: Public domain | W3C validator |