Theorem dffn4 6801

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540  ran crn 5660   Fn wfn 6531  –onto→wfo 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-fo 6542

This theorem is referenced by:  funforn  6802  fimadmfo  6804  ffoss  7949  tposf2  8254  rneqdmfinf1o  9350  fidomdm  9351  indexfi  9377  intrnfi  9433  fifo  9449  ixpiunwdom  9609  infpwfien  10081  infmap2  10236  cfflb  10278  cfslb2n  10287  ttukeylem6  10533  dmct  10543  fnrndomg  10555  rankcf  10796  tskuni  10802  tskurn  10808  fseqsupcl  14000  s7f1o  14990  vdwlem6  17011  0ram2  17046  0ramcl  17048  quslem  17562  gsumval3  19893  gsumzoppg  19930  mplsubrglem  21969  rncmp  23339  cmpsub  23343  tgcmp  23344  hauscmplem  23349  conncn  23369  2ndcctbss  23398  2ndcomap  23401  2ndcsep  23402  comppfsc  23475  ptcnplem  23564  txtube  23583  txcmplem1  23584  tx1stc  23593  tx2ndc  23594  qtopid  23648  qtopcmplem  23650  qtopkgen  23653  kqtopon  23670  kqopn  23677  kqcld  23678  qtopf1  23759  rnelfm  23896  fmfnfmlem2  23898  fmfnfm  23901  alexsubALT  23994  ptcmplem2  23996  tmdgsum2  24039  tsmsxplem1  24096  met1stc  24465  met2ndci  24466  uniiccdif  25536  dyadmbl  25558  mbfimaopnlem  25613  i1fadd  25653  i1fmul  25654  i1fmulc  25661  mbfi1fseqlem4  25676  limciun  25852  aannenlem3  26295  efabl  26516  logccv  26629  locfinreflem  33876  mvrsfpw  35533  msrfo  35573  mtyf  35579  bj-inftyexpitaufo  37225  itg2addnclem2  37701  istotbnd3  37800  sstotbnd  37804  prdsbnd  37822  cntotbnd  37825  heiborlem1  37840  heibor  37850  dihintcl  41368  focofob  47089