Theorem dffn4 6425

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

Syntax hints:   ↔ wb 198   ∧ wa 387   = wceq 1507  ran crn 5408   Fn wfn 6183  –onto→wfo 6186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-9 2059  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2771  df-fo 6194

This theorem is referenced by:  funforn  6426  fimadmfo  6428  ffoss  7459  tposf2  7719  rneqdmfinf1o  8595  fidomdm  8596  pwfilem  8613  indexfi  8627  intrnfi  8675  fifo  8691  ixpiunwdom  8850  infpwfien  9282  infmap2  9438  cfflb  9479  cfslb2n  9488  ttukeylem6  9734  dmct  9744  fnrndomg  9756  rankcf  9997  tskuni  10003  tskurn  10009  fseqsupcl  13160  vdwlem6  16178  0ram2  16213  0ramcl  16215  quslem  16672  gsumval3  18781  gsumzoppg  18817  mplsubrglem  19933  rncmp  21708  cmpsub  21712  tgcmp  21713  hauscmplem  21718  conncn  21738  2ndcctbss  21767  2ndcomap  21770  2ndcsep  21771  comppfsc  21844  ptcnplem  21933  txtube  21952  txcmplem1  21953  tx1stc  21962  tx2ndc  21963  qtopid  22017  qtopcmplem  22019  qtopkgen  22022  kqtopon  22039  kqopn  22046  kqcld  22047  qtopf1  22128  rnelfm  22265  fmfnfmlem2  22267  fmfnfm  22270  alexsubALT  22363  ptcmplem2  22365  tmdgsum2  22408  tsmsxplem1  22464  met1stc  22834  met2ndci  22835  uniiccdif  23882  dyadmbl  23904  mbfimaopnlem  23959  i1fadd  23999  i1fmul  24000  itg1addlem4  24003  i1fmulc  24007  mbfi1fseqlem4  24022  limciun  24195  aannenlem3  24622  efabl  24835  logccv  24947  locfinreflem  30754  mvrsfpw  32279  msrfo  32319  mtyf  32325  bj-inftyexpitaufo  33959  itg2addnclem2  34391  istotbnd3  34497  sstotbnd  34501  prdsbnd  34519  cntotbnd  34522  heiborlem1  34537  heibor  34547  dihintcl  37931