Theorem dffn4 6753

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 2737	. . 3 ⊢ ran 𝐹 = ran 𝐹
2	1	biantru 529	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
3		df-fo 6499	. 2 ⊢ (𝐹:𝐴–onto→ran 𝐹 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
4	2, 3	bitr4i 278	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴–onto→ran 𝐹)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542  ran crn 5626   Fn wfn 6488  –onto→wfo 6491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-fo 6499

This theorem is referenced by:  funforn  6754  fimadmfo  6756  ffoss  7893  tposf2  8195  rneqdmfinf1o  9238  fidomdm  9239  indexfi  9265  intrnfi  9324  fifo  9340  ixpiunwdom  9500  infpwfien  9977  infmap2  10132  cfflb  10174  cfslb2n  10183  ttukeylem6  10429  dmct  10439  fnrndomg  10451  rankcf  10693  tskuni  10699  tskurn  10705  fseqsupcl  13905  s7f1o  14894  vdwlem6  16919  0ram2  16954  0ramcl  16956  quslem  17469  gsumval3  19841  gsumzoppg  19878  mplsubrglem  21964  rncmp  23345  cmpsub  23349  tgcmp  23350  hauscmplem  23355  conncn  23375  2ndcctbss  23404  2ndcomap  23407  2ndcsep  23408  comppfsc  23481  ptcnplem  23570  txtube  23589  txcmplem1  23590  tx1stc  23599  tx2ndc  23600  qtopid  23654  qtopcmplem  23656  qtopkgen  23659  kqtopon  23676  kqopn  23683  kqcld  23684  qtopf1  23765  rnelfm  23902  fmfnfmlem2  23904  fmfnfm  23907  alexsubALT  24000  ptcmplem2  24002  tmdgsum2  24045  tsmsxplem1  24102  met1stc  24470  met2ndci  24471  uniiccdif  25540  dyadmbl  25562  mbfimaopnlem  25617  i1fadd  25657  i1fmul  25658  i1fmulc  25665  mbfi1fseqlem4  25680  limciun  25856  aannenlem3  26299  efabl  26520  logccv  26633  locfinreflem  34010  mvrsfpw  35713  msrfo  35753  mtyf  35759  bj-inftyexpitaufo  37420  itg2addnclem2  37886  istotbnd3  37985  sstotbnd  37989  prdsbnd  38007  cntotbnd  38010  heiborlem1  38025  heibor  38035  dihintcl  41683  focofob  47403