Theorem dffn4 6778

Description: A function maps onto its range. (Contributed by NM, 10-May-1998.)

Assertion

Ref	Expression
dffn4	⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹)

Proof of Theorem dffn4

Step	Hyp	Ref	Expression
1		eqid 2729	. . 3 ⊢ ran 𝐹 = ran 𝐹
2	1	biantru 529	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
3		df-fo 6517	. 2 ⊢ (𝐹:𝐴–onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
4	2, 3	bitr4i 278	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540  ran crn 5639   Fn wfn 6506  –onto→wfo 6509

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 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-fo 6517

This theorem is referenced by:  funforn  6779  fimadmfo  6781  ffoss  7924  tposf2  8229  rneqdmfinf1o  9284  fidomdm  9285  indexfi  9311  intrnfi  9367  fifo  9383  ixpiunwdom  9543  infpwfien  10015  infmap2  10170  cfflb  10212  cfslb2n  10221  ttukeylem6  10467  dmct  10477  fnrndomg  10489  rankcf  10730  tskuni  10736  tskurn  10742  fseqsupcl  13942  s7f1o  14932  vdwlem6  16957  0ram2  16992  0ramcl  16994  quslem  17506  gsumval3  19837  gsumzoppg  19874  mplsubrglem  21913  rncmp  23283  cmpsub  23287  tgcmp  23288  hauscmplem  23293  conncn  23313  2ndcctbss  23342  2ndcomap  23345  2ndcsep  23346  comppfsc  23419  ptcnplem  23508  txtube  23527  txcmplem1  23528  tx1stc  23537  tx2ndc  23538  qtopid  23592  qtopcmplem  23594  qtopkgen  23597  kqtopon  23614  kqopn  23621  kqcld  23622  qtopf1  23703  rnelfm  23840  fmfnfmlem2  23842  fmfnfm  23845  alexsubALT  23938  ptcmplem2  23940  tmdgsum2  23983  tsmsxplem1  24040  met1stc  24409  met2ndci  24410  uniiccdif  25479  dyadmbl  25501  mbfimaopnlem  25556  i1fadd  25596  i1fmul  25597  i1fmulc  25604  mbfi1fseqlem4  25619  limciun  25795  aannenlem3  26238  efabl  26459  logccv  26572  locfinreflem  33830  mvrsfpw  35493  msrfo  35533  mtyf  35539  bj-inftyexpitaufo  37190  itg2addnclem2  37666  istotbnd3  37765  sstotbnd  37769  prdsbnd  37787  cntotbnd  37790  heiborlem1  37805  heibor  37815  dihintcl  41338  focofob  47081