Theorem dffn4 6747

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 2735	. . 3 ⊢ ran 𝐹 = ran 𝐹
2	1	biantru 529	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
3		df-fo 6493	. 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 5621   Fn wfn 6482  –onto→wfo 6485

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2727  df-fo 6493

This theorem is referenced by:  funforn  6748  fimadmfo  6750  ffoss  7888  tposf2  8189  rneqdmfinf1o  9232  fidomdm  9233  indexfi  9259  intrnfi  9318  fifo  9334  ixpiunwdom  9494  infpwfien  9973  infmap2  10128  cfflb  10170  cfslb2n  10179  ttukeylem6  10425  dmct  10435  fnrndomg  10447  rankcf  10689  tskuni  10695  tskurn  10701  fseqsupcl  13928  s7f1o  14917  vdwlem6  16946  0ram2  16981  0ramcl  16983  quslem  17496  gsumval3  19871  gsumzoppg  19908  mplsubrglem  21971  rncmp  23349  cmpsub  23353  tgcmp  23354  hauscmplem  23359  conncn  23379  2ndcctbss  23408  2ndcomap  23411  2ndcsep  23412  comppfsc  23485  ptcnplem  23574  txtube  23593  txcmplem1  23594  tx1stc  23603  tx2ndc  23604  qtopid  23658  qtopcmplem  23660  qtopkgen  23663  kqtopon  23680  kqopn  23687  kqcld  23688  qtopf1  23769  rnelfm  23906  fmfnfmlem2  23908  fmfnfm  23911  alexsubALT  24004  ptcmplem2  24006  tmdgsum2  24049  tsmsxplem1  24106  met1stc  24474  met2ndci  24475  uniiccdif  25533  dyadmbl  25555  mbfimaopnlem  25610  i1fadd  25650  i1fmul  25651  i1fmulc  25658  mbfi1fseqlem4  25673  limciun  25849  aannenlem3  26284  efabl  26502  logccv  26615  locfinreflem  33972  mvrsfpw  35676  msrfo  35716  mtyf  35722  bj-inftyexpitaufo  37504  itg2addnclem2  37981  istotbnd3  38080  sstotbnd  38084  prdsbnd  38102  cntotbnd  38105  heiborlem1  38120  heibor  38130  dihintcl  41778  focofob  47516