Theorem dffn4 6798

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 400   = wceq 1569  ran crn 5661   Fn wfn 6531  –onto→wfo 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754  df-fo 6542

This theorem is used by:  funforn  6799  fimadmfo  6801  ffoss  7941  tposf2  8244  rneqdmfinf1o  9288  fidomdm  9289  indexfi  9315  intrnfi  9374  fifo  9390  ixpiunwdom  9550  infpwfien  10053  infmap2  10207  cfflb  10249  cfslb2n  10258  ttukeylem6  10504  dmct  10514  fnrndomg  10526  rankcf  10768  tskuni  10774  tskurn  10780  fseqsupcl  14020  s7f1o  15010  vdwlem6  17052  0ram2  17087  0ramcl  17089  quslem  17603  gsumval3  19983  gsumzoppg  20020  mplsubrglem  22164  rncmp  23564  cmpsub  23568  tgcmp  23569  hauscmplem  23574  conncn  23594  2ndcctbss  23623  2ndcomap  23626  2ndcsep  23627  comppfsc  23700  ptcnplem  23789  txtube  23808  txcmplem1  23809  tx1stc  23818  tx2ndc  23819  qtopid  23873  qtopcmplem  23875  qtopkgen  23878  kqtopon  23895  kqopn  23902  kqcld  23903  qtopf1  23984  rnelfm  24121  fmfnfmlem2  24123  fmfnfm  24126  alexsubALT  24219  ptcmplem2  24221  tmdgsum2  24264  tsmsxplem1  24321  met1stc  24689  met2ndci  24690  uniiccdif  25748  dyadmbl  25770  mbfimaopnlem  25825  i1fadd  25865  i1fmul  25866  i1fmulc  25873  mbfi1fseqlem4  25888  limciun  26064  aannenlem3  26504  efabl  26726  logccv  26839  locfinreflem  34239  mvrsfpw  36006  msrfo  36046  mtyf  36052  bj-inftyexpitaufo  37874  itg2addnclem2  38351  istotbnd3  38450  sstotbnd  38454  prdsbnd  38472  cntotbnd  38475  heiborlem1  38490  heibor  38500  dihintcl  42146  focofob  47845