Theorem dffn4 6799

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 2762	. . 3 ⊢ ran 𝐹 = ran 𝐹
2	1	biantru 539	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = ran 𝐹))
3		df-fo 6543	. 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 5660   Fn wfn 6532  –onto→wfo 6535

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 2734

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

This theorem is used by:  funforn  6800  fimadmfo  6802  ffoss  7946  tposf2  8251  rneqdmfinf1o  9303  fidomdm  9304  indexfi  9330  intrnfi  9389  fifo  9405  ixpiunwdom  9565  infpwfien  10068  infmap2  10222  cfflb  10264  cfslb2n  10273  ttukeylem6  10519  dmct  10529  dmctOLD  10530  imadomnum  10541  fnrndomnum  10544  fnrndomgOLD  10546  rankcf  10789  tskuni  10795  tskurn  10801  fseqsupcl  14043  s7f1o  15041  vdwlem6  17082  0ram2  17117  0ramcl  17119  quslem  17633  gsumval3  20035  gsumzoppg  20072  mplsubrglem  22219  rncmp  23622  cmpsub  23626  tgcmp  23627  hauscmplem  23632  conncn  23652  2ndcctbss  23682  2ndcomap  23685  2ndcsep  23686  comppfsc  23759  ptcnplem  23848  txtube  23867  txcmplem1  23868  tx1stc  23877  tx2ndc  23878  qtopid  23932  qtopcmplem  23934  qtopkgen  23937  kqtopon  23954  kqopn  23961  kqcld  23962  qtopf1  24043  rnelfm  24180  fmfnfmlem2  24182  fmfnfm  24185  alexsubALT  24278  ptcmplem2  24280  tmdgsum2  24323  tsmsxplem1  24380  met1stc  24748  met2ndci  24749  uniiccdif  25807  dyadmbl  25829  mbfimaopnlem  25884  i1fadd  25924  i1fmul  25925  i1fmulc  25932  mbfi1fseqlem4  25947  limciun  26123  aannenlem3  26563  efabl  26785  logccv  26898  locfinreflem  34337  mvrsfpw  36072  msrfo  36112  mtyf  36118  bj-inftyexpitaufo  37941  itg2addnclem2  38408  istotbnd3  38508  sstotbnd  38512  prdsbnd  38530  cntotbnd  38533  heiborlem1  38548  heibor  38558  dihintcl  42204  focofob  47955