Theorem dffn4 6571

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

Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538  ran crn 5520   Fn wfn 6319  –onto→wfo 6322

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-fo 6330

This theorem is referenced by:  funforn  6572  fimadmfo  6574  ffoss  7629  tposf2  7899  rneqdmfinf1o  8784  fidomdm  8785  pwfilem  8802  indexfi  8816  intrnfi  8864  fifo  8880  ixpiunwdom  9038  infpwfien  9473  infmap2  9629  cfflb  9670  cfslb2n  9679  ttukeylem6  9925  dmct  9935  fnrndomg  9947  rankcf  10188  tskuni  10194  tskurn  10200  fseqsupcl  13340  vdwlem6  16312  0ram2  16347  0ramcl  16349  quslem  16808  gsumval3  19020  gsumzoppg  19057  mplsubrglem  20677  rncmp  22001  cmpsub  22005  tgcmp  22006  hauscmplem  22011  conncn  22031  2ndcctbss  22060  2ndcomap  22063  2ndcsep  22064  comppfsc  22137  ptcnplem  22226  txtube  22245  txcmplem1  22246  tx1stc  22255  tx2ndc  22256  qtopid  22310  qtopcmplem  22312  qtopkgen  22315  kqtopon  22332  kqopn  22339  kqcld  22340  qtopf1  22421  rnelfm  22558  fmfnfmlem2  22560  fmfnfm  22563  alexsubALT  22656  ptcmplem2  22658  tmdgsum2  22701  tsmsxplem1  22758  met1stc  23128  met2ndci  23129  uniiccdif  24182  dyadmbl  24204  mbfimaopnlem  24259  i1fadd  24299  i1fmul  24300  itg1addlem4  24303  i1fmulc  24307  mbfi1fseqlem4  24322  limciun  24497  aannenlem3  24926  efabl  25142  logccv  25254  locfinreflem  31193  mvrsfpw  32866  msrfo  32906  mtyf  32912  bj-inftyexpitaufo  34617  itg2addnclem2  35109  istotbnd3  35209  sstotbnd  35213  prdsbnd  35231  cntotbnd  35234  heiborlem1  35249  heibor  35259  dihintcl  38640