Theorem frn 5488

Description: The range of a mapping. (Contributed by NM, 3-Aug-1994.)

Assertion

Ref	Expression
frn	⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)

Proof of Theorem frn

Step	Hyp	Ref	Expression
1		df-f 5328	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2	1	simprbi 275	1 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3198  ran crn 4724   Fn wfn 5319  ⟶wf 5320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem depends on definitions:  df-bi 117  df-f 5328

This theorem is referenced by:  frnd  5489  fimass  5495  fco2  5498  fssxp  5499  fimacnvdisj  5518  f00  5525  f0rn0  5528  f1rn  5540  f1ff1  5547  fimacnv  5772  ffvelcdm  5776  f1ompt  5794  fnfvrnss  5803  rnmptss  5804  fliftrel  5928  fo1stresm  6319  fo2ndresm  6320  1stcof  6321  2ndcof  6322  fo2ndf  6387  tposf2  6429  iunon  6445  smores2  6455  map0b  6851  mapsn  6854  f1imaen2g  6962  phplem4dom  7043  isinfinf  7079  updjudhcoinlf  7270  updjudhcoinrg  7271  casef  7278  unirnioo  10198  frecuzrdgdomlem  10669  frecuzrdgfunlem  10671  frecuzrdgtclt  10673  ennnfonelemrn  13030  ctinf  13041  txuni2  14970  blin2  15146  tgqioo  15269  reeff1o  15487  usgredgssen  16001