Theorem fimass 6679

Description: The image of a class under a function with domain and codomain is a subset of its codomain. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Assertion

Ref	Expression
fimass	⊢ (𝐹:𝐴⟶𝐵 → (𝐹 “ 𝑋) ⊆ 𝐵)

Proof of Theorem fimass

Step	Hyp	Ref	Expression
1		imassrn 6030	. 2 ⊢ (𝐹 “ 𝑋) ⊆ ran 𝐹
2		frn 6666	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
3	1, 2	sstrid 3928	1 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 “ 𝑋) ⊆ 𝐵)

Syntax hints:   → wi 4   ⊆ wss 3885  ran crn 5622   “ cima 5624  ⟶wf 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-br 5076  df-opab 5138  df-xp 5627  df-cnv 5629  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-f 6493

This theorem is referenced by:  fimassd  6680  fimarab  6905  f1imaen2g  8956  domunsncan  9009  fissuni  9261  fipreima  9262  carduniima  10013  psgnunilem1  19463  fbasrn  23871  imaelfm  23938  wlkres  29759  trlreslem  29788  tocyccntz  33229  rhmimaidl  33519  nummin  35289  regsfromunir1  36783  hashscontpowcl  42620  relpfrlem  45412  limsupvaluz  46165  fundcmpsurbijinjpreimafv  47896  fundcmpsurinjimaid  47900