Theorem rnmptss 7070

Description: The range of an operation given by the maps-to notation as a subset. (Contributed by Thierry Arnoux, 24-Sep-2017.)

Hypothesis

Ref	Expression
rnmptss.1	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)

Assertion

Ref	Expression
rnmptss	⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶

Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem rnmptss

Step	Hyp	Ref	Expression
1		rnmptss.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
2	1	fmpt 7057	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ 𝐹:𝐴⟶𝐶)
3		frn 6670	. 2 ⊢ (𝐹:𝐴⟶𝐶 → ran 𝐹 ⊆ 𝐶)
4	2, 3	sylbi 217	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∀wral 3052   ⊆ wss 3890   ↦ cmpt 5167  ran crn 5626  ⟶wf 6489

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-fun 6495  df-fn 6496  df-f 6497

This theorem is referenced by:  rnmptssd  7071  mptexw  7900  iunon  8273  iinon  8274  gruiun  10716  subdrgint  20774  smadiadetlem3lem2  22645  tgiun  22957  ustuqtop0  24218  metustss  24529  efabl  26530  efsubm  26531  fnpreimac  32761  prodindf  32940  swrdrn2  33032  gsummpt2co  33127  psgnfzto1stlem  33179  elrgspnsubrunlem1  33326  nsgmgc  33490  nsgqusf1olem1  33491  algextdeglem2  33881  algextdeglem4  33883  locfinreflem  34003  rspectopn  34030  zarcls  34037  zartopn  34038  gsumesum  34222  esumlub  34223  esumgect  34253  esum2d  34256  ldgenpisyslem1  34326  sxbrsigalem0  34434  omscl  34458  omsmon  34461  carsgclctunlem2  34482  carsgclctunlem3  34483  pmeasadd  34488  hgt750lemb  34819  mnurndlem2  44730  suprnmpt  45625  rnmptssrn  45633  wessf1ornlem  45636  rnmptssbi  45710  liminflelimsuplem  46224  fourierdlem53  46608  fourierdlem111  46666  ioorrnopnlem  46753  salexct3  46791  salgensscntex  46793  sge0rnre  46813  sge0tsms  46829  sge0cl  46830  sge0fsum  46836  sge0sup  46840  sge0gerp  46844  sge0pnffigt  46845  sge0lefi  46847  sge0xaddlem1  46882  sge0xaddlem2  46883  meadjiunlem  46914  sinnpoly  47354