Theorem dffn4 6790

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ran crn 5648   Fn wfn 6522  –onto→wfo 6525

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-fo 6533

This theorem is used by:  funforn  6791  fimadmfo  6793  ffoss  7941  tposf2  8245  rneqdmfinf1o  9300  fidomdm  9301  indexfi  9327  intrnfi  9386  fifo  9402  ixpiunwdom  9562  infpwfien  10112  infmap2  10266  cfflb  10308  cfslb2n  10317  ttukeylem6  10563  dmct  10573  dmctOLD  10574  imadomnum  10585  fnrndomnum  10588  fnrndomgOLD  10590  rankcf  10833  tskuni  10839  tskurn  10845  fseqsupcl  14088  s7f1o  15086  vdwlem6  17125  0ram2  17160  0ramcl  17162  quslem  17676  gsumval3  20082  gsumzoppg  20119  mplsubrglem  22272  rncmp  23675  cmpsub  23679  tgcmp  23680  hauscmplem  23685  conncn  23705  2ndcctbss  23735  2ndcomap  23738  2ndcsep  23739  comppfsc  23812  ptcnplem  23901  txtube  23920  txcmplem1  23921  tx1stc  23930  tx2ndc  23931  qtopid  23985  qtopcmplem  23987  qtopkgen  23990  kqtopon  24007  kqopn  24014  kqcld  24015  qtopf1  24096  rnelfm  24233  fmfnfmlem2  24235  fmfnfm  24238  alexsubALT  24331  ptcmplem2  24333  tmdgsum2  24376  tsmsxplem1  24433  met1stc  24801  met2ndci  24802  uniiccdif  25860  dyadmbl  25882  mbfimaopnlem  25937  i1fadd  25977  i1fmul  25978  i1fmulc  25985  mbfi1fseqlem4  26000  limciun  26175  aannenlem3  26620  efabl  26841  logccv  26954  locfinreflem  34405  mvrsfpw  36192  msrfo  36232  mtyf  36238  bj-inftyexpitaufo  38043  itg2addnclem2  38510  istotbnd3  38625  sstotbnd  38629  prdsbnd  38647  cntotbnd  38650  heiborlem1  38665  heibor  38675  dihintcl  42321  focofob  48072