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  7892  tposf2  8194  rneqdmfinf1o  9237  fidomdm  9238  indexfi  9264  intrnfi  9323  fifo  9339  ixpiunwdom  9499  infpwfien  9976  infmap2  10131  cfflb  10173  cfslb2n  10182  ttukeylem6  10428  dmct  10438  fnrndomg  10450  rankcf  10692  tskuni  10698  tskurn  10704  fseqsupcl  13904  s7f1o  14893  vdwlem6  16918  0ram2  16953  0ramcl  16955  quslem  17468  gsumval3  19840  gsumzoppg  19877  mplsubrglem  21963  rncmp  23344  cmpsub  23348  tgcmp  23349  hauscmplem  23354  conncn  23374  2ndcctbss  23403  2ndcomap  23406  2ndcsep  23407  comppfsc  23480  ptcnplem  23569  txtube  23588  txcmplem1  23589  tx1stc  23598  tx2ndc  23599  qtopid  23653  qtopcmplem  23655  qtopkgen  23658  kqtopon  23675  kqopn  23682  kqcld  23683  qtopf1  23764  rnelfm  23901  fmfnfmlem2  23903  fmfnfm  23906  alexsubALT  23999  ptcmplem2  24001  tmdgsum2  24044  tsmsxplem1  24101  met1stc  24469  met2ndci  24470  uniiccdif  25539  dyadmbl  25561  mbfimaopnlem  25616  i1fadd  25656  i1fmul  25657  i1fmulc  25664  mbfi1fseqlem4  25679  limciun  25855  aannenlem3  26298  efabl  26519  logccv  26632  locfinreflem  33978  mvrsfpw  35681  msrfo  35721  mtyf  35727  bj-inftyexpitaufo  37378  itg2addnclem2  37844  istotbnd3  37943  sstotbnd  37947  prdsbnd  37965  cntotbnd  37968  heiborlem1  37983  heibor  37993  dihintcl  41641  focofob  47362