Theorem frn 3740

Description: The range of a mapping.

Assertion

Ref	Expression
frn	⊢ (F:A–→B → ran F ⊆ B)

Proof of Theorem frn

Step	Hyp	Ref	Expression
1		df-f 3275	. 2 ⊢ (F:A–→B ↔ (F Fn A ⋀ ran F ⊆ B))
2	1	pm3.27bi 324	1 ⊢ (F:A–→B → ran F ⊆ B)

Syntax hints:   → wi 3   ⊆ wss 2099  ran crn 3252   Fn wfn 3258  –→wf 3259

This theorem is referenced by:  fss 3742  fco 3743  fssxp 3744  fimacnvdisj 3756  f00 3764  foconst 3791  f1dmex 3821  fimacnv 3924  ffvelrn 3928  rnssopab 3939  fnfvrnss 3944  fo1stres 4156  fo2ndres 4157  1stcof 4160  map0b 4484  mapsn 4486  fodomr 4628  mapenlem2 4637  inf3lem7 4764  carduniima 5040  unirnioo 6529  fsequb2 6655  fseqsupcl 6656  fseqsupubi 6657  seq1ublem 7114  climsupi 7358  cvgcmpubi 7389  ruclem17 7738  ruclem33 7754  cncfmet1 8117  grplactf1o 8339  ghsubgi 8379  hhssims 9421  kbass5 10333  ghomgrpilem2 10671  ghomfo 10676  cayleylem2 10695  bwt2 11123  rdmob 11202  rcmob 11203  hartog 11436  cncls 11473  cnsubsp 11483  compsub 11488  alexsub 11500  2ndcctbss 11539  comppfsc 11578  cnpfillim 11686  elfilmap 11690  fmf 11693  fmbas 11694  imaelfm 11695  filmapss 11696  fcluscnplem 11729  tailuni 11761  filnet 11768  gafo 11773  fnopabco 11810  oprabco 11811  upxp 11822  upixp 11823  indexd 11846  cnresima 11952  uptx 11978  txcnopab 11980  ismtyres 12010  heiborlem15 12025  heiborlem17 12027  reheibor 12081  phtpyid 12091  phtpycolem4 12096

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 145  df-an 223  df-f 3275

Copyright terms: Public domain