Theorem dffn4 6827

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1537  ran crn 5690   Fn wfn 6558  –onto→wfo 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-fo 6569

This theorem is referenced by:  funforn  6828  fimadmfo  6830  ffoss  7969  tposf2  8274  rneqdmfinf1o  9371  fidomdm  9372  indexfi  9398  intrnfi  9454  fifo  9470  ixpiunwdom  9628  infpwfien  10100  infmap2  10255  cfflb  10297  cfslb2n  10306  ttukeylem6  10552  dmct  10562  fnrndomg  10574  rankcf  10815  tskuni  10821  tskurn  10827  fseqsupcl  14015  s7f1o  15002  vdwlem6  17020  0ram2  17055  0ramcl  17057  quslem  17590  gsumval3  19940  gsumzoppg  19977  mplsubrglem  22042  rncmp  23420  cmpsub  23424  tgcmp  23425  hauscmplem  23430  conncn  23450  2ndcctbss  23479  2ndcomap  23482  2ndcsep  23483  comppfsc  23556  ptcnplem  23645  txtube  23664  txcmplem1  23665  tx1stc  23674  tx2ndc  23675  qtopid  23729  qtopcmplem  23731  qtopkgen  23734  kqtopon  23751  kqopn  23758  kqcld  23759  qtopf1  23840  rnelfm  23977  fmfnfmlem2  23979  fmfnfm  23982  alexsubALT  24075  ptcmplem2  24077  tmdgsum2  24120  tsmsxplem1  24177  met1stc  24550  met2ndci  24551  uniiccdif  25627  dyadmbl  25649  mbfimaopnlem  25704  i1fadd  25744  i1fmul  25745  itg1addlem4OLD  25749  i1fmulc  25753  mbfi1fseqlem4  25768  limciun  25944  aannenlem3  26387  efabl  26607  logccv  26720  locfinreflem  33801  mvrsfpw  35491  msrfo  35531  mtyf  35537  bj-inftyexpitaufo  37185  itg2addnclem2  37659  istotbnd3  37758  sstotbnd  37762  prdsbnd  37780  cntotbnd  37783  heiborlem1  37798  heibor  37808  dihintcl  41327  focofob  47030