| 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 2737 | . . 3 ⊢ ran 𝐹 = ran 𝐹 | |
| 2 | 1 | biantru 529 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹)) |
| 3 | df-fo 6567 | . 2 ⊢ (𝐹:𝐴–onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹)) | |
| 4 | 2, 3 | bitr4i 278 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1540 ran crn 5686 Fn wfn 6556 –onto→wfo 6559 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-fo 6567 |
| This theorem is referenced by: funforn 6827 fimadmfo 6829 ffoss 7970 tposf2 8275 rneqdmfinf1o 9373 fidomdm 9374 indexfi 9400 intrnfi 9456 fifo 9472 ixpiunwdom 9630 infpwfien 10102 infmap2 10257 cfflb 10299 cfslb2n 10308 ttukeylem6 10554 dmct 10564 fnrndomg 10576 rankcf 10817 tskuni 10823 tskurn 10829 fseqsupcl 14018 s7f1o 15005 vdwlem6 17024 0ram2 17059 0ramcl 17061 quslem 17588 gsumval3 19925 gsumzoppg 19962 mplsubrglem 22024 rncmp 23404 cmpsub 23408 tgcmp 23409 hauscmplem 23414 conncn 23434 2ndcctbss 23463 2ndcomap 23466 2ndcsep 23467 comppfsc 23540 ptcnplem 23629 txtube 23648 txcmplem1 23649 tx1stc 23658 tx2ndc 23659 qtopid 23713 qtopcmplem 23715 qtopkgen 23718 kqtopon 23735 kqopn 23742 kqcld 23743 qtopf1 23824 rnelfm 23961 fmfnfmlem2 23963 fmfnfm 23966 alexsubALT 24059 ptcmplem2 24061 tmdgsum2 24104 tsmsxplem1 24161 met1stc 24534 met2ndci 24535 uniiccdif 25613 dyadmbl 25635 mbfimaopnlem 25690 i1fadd 25730 i1fmul 25731 i1fmulc 25738 mbfi1fseqlem4 25753 limciun 25929 aannenlem3 26372 efabl 26592 logccv 26705 locfinreflem 33839 mvrsfpw 35511 msrfo 35551 mtyf 35557 bj-inftyexpitaufo 37203 itg2addnclem2 37679 istotbnd3 37778 sstotbnd 37782 prdsbnd 37800 cntotbnd 37803 heiborlem1 37818 heibor 37828 dihintcl 41346 focofob 47092 |
| Copyright terms: Public domain | W3C validator |