Theorem rnmptss 7069

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 7056	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ 𝐹:𝐴⟶𝐶)
3		frn 6669	. 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 5625  ⟶wf 6488

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 5231  ax-pr 5370

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 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  rnmptssd  7070  mptexw  7899  iunon  8272  iinon  8273  gruiun  10713  subdrgint  20771  smadiadetlem3lem2  22642  tgiun  22954  ustuqtop0  24215  metustss  24526  efabl  26527  efsubm  26528  fnpreimac  32758  prodindf  32937  swrdrn2  33029  gsummpt2co  33124  psgnfzto1stlem  33176  elrgspnsubrunlem1  33323  nsgmgc  33487  nsgqusf1olem1  33488  algextdeglem2  33878  algextdeglem4  33880  locfinreflem  34000  rspectopn  34027  zarcls  34034  zartopn  34035  gsumesum  34219  esumlub  34220  esumgect  34250  esum2d  34253  ldgenpisyslem1  34323  sxbrsigalem0  34431  omscl  34455  omsmon  34458  carsgclctunlem2  34479  carsgclctunlem3  34480  pmeasadd  34485  hgt750lemb  34816  mnurndlem2  44727  suprnmpt  45622  rnmptssrn  45630  wessf1ornlem  45633  rnmptssbi  45707  liminflelimsuplem  46221  fourierdlem53  46605  fourierdlem111  46663  ioorrnopnlem  46750  salexct3  46788  salgensscntex  46790  sge0rnre  46810  sge0tsms  46826  sge0cl  46827  sge0fsum  46833  sge0sup  46837  sge0gerp  46841  sge0pnffigt  46842  sge0lefi  46844  sge0xaddlem1  46879  sge0xaddlem2  46880  meadjiunlem  46911  sinnpoly  47351