Theorem rnmptss 7068

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 7055	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ 𝐹:𝐴⟶𝐶)
3		frn 6669	. 2 ⊢ (𝐹:𝐴⟶𝐶 → ran 𝐹 ⊆ 𝐶)
4	2, 3	sylbi 217	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∀wral 3051   ⊆ wss 3901   ↦ cmpt 5179  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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-mpt 5180  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:  mptexw  7897  iunon  8271  iinon  8272  gruiun  10710  subdrgint  20736  smadiadetlem3lem2  22611  tgiun  22923  ustuqtop0  24184  metustss  24495  efabl  26515  efsubm  26516  fnpreimac  32749  prodindf  32944  swrdrn2  33036  gsummpt2co  33131  psgnfzto1stlem  33182  elrgspnsubrunlem1  33329  nsgmgc  33493  nsgqusf1olem1  33494  algextdeglem2  33875  algextdeglem4  33877  locfinreflem  33997  rspectopn  34024  zarcls  34031  zartopn  34032  gsumesum  34216  esumlub  34217  esumgect  34247  esum2d  34250  ldgenpisyslem1  34320  sxbrsigalem0  34428  omscl  34452  omsmon  34455  carsgclctunlem2  34476  carsgclctunlem3  34477  pmeasadd  34482  hgt750lemb  34813  mnurndlem2  44523  suprnmpt  45418  rnmptssrn  45426  wessf1ornlem  45429  rnmptssd  45440  rnmptssbi  45504  liminflelimsuplem  46019  fourierdlem53  46403  fourierdlem111  46461  ioorrnopnlem  46548  salexct3  46586  salgensscntex  46588  sge0rnre  46608  sge0tsms  46624  sge0cl  46625  sge0fsum  46631  sge0sup  46635  sge0gerp  46639  sge0pnffigt  46640  sge0lefi  46642  sge0xaddlem1  46677  sge0xaddlem2  46678  meadjiunlem  46709  sinnpoly  47137