Theorem dffn4 6769

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

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1550  ran crn 5637   Fn wfn 6501  –onto→wfo 6504

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-cleq 2744  df-fo 6512

This theorem is referenced by:  funforn  6770  fimadmfo  6772  ffoss  7912  tposf2  8214  rneqdmfinf1o  9262  fidomdm  9263  indexfi  9289  intrnfi  9348  fifo  9364  ixpiunwdom  9524  infpwfien  10004  infmap2  10159  cfflb  10202  cfslb2n  10211  ttukeylem6  10457  dmct  10467  fnrndomg  10479  rankcf  10721  tskuni  10727  tskurn  10733  fseqsupcl  13976  s7f1o  14965  vdwlem6  16994  0ram2  17029  0ramcl  17031  quslem  17545  gsumval3  19919  gsumzoppg  19956  mplsubrglem  22024  rncmp  23425  cmpsub  23429  tgcmp  23430  hauscmplem  23435  conncn  23455  2ndcctbss  23484  2ndcomap  23487  2ndcsep  23488  comppfsc  23561  ptcnplem  23650  txtube  23669  txcmplem1  23670  tx1stc  23679  tx2ndc  23680  qtopid  23734  qtopcmplem  23736  qtopkgen  23739  kqtopon  23756  kqopn  23763  kqcld  23764  qtopf1  23845  rnelfm  23982  fmfnfmlem2  23984  fmfnfm  23987  alexsubALT  24080  ptcmplem2  24082  tmdgsum2  24125  tsmsxplem1  24182  met1stc  24550  met2ndci  24551  uniiccdif  25609  dyadmbl  25631  mbfimaopnlem  25686  i1fadd  25726  i1fmul  25727  i1fmulc  25734  mbfi1fseqlem4  25749  limciun  25925  aannenlem3  26360  efabl  26581  logccv  26694  locfinreflem  34081  mvrsfpw  35794  msrfo  35834  mtyf  35840  bj-inftyexpitaufo  37632  itg2addnclem2  38109  istotbnd3  38208  sstotbnd  38212  prdsbnd  38230  cntotbnd  38233  heiborlem1  38248  heibor  38258  dihintcl  41906  focofob  47612