Theorem rnmptss 7142

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  ∀wral 3058   ⊆ wss 3962   ↦ cmpt 5230  ran crn 5689  ⟶wf 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-fun 6564  df-fn 6565  df-f 6566

This theorem is referenced by:  mptexw  7975  iunon  8377  iinon  8378  gruiun  10836  subdrgint  20820  smadiadetlem3lem2  22688  tgiun  23001  ustuqtop0  24264  metustss  24579  efabl  26606  efsubm  26607  fnpreimac  32687  swrdrn2  32923  gsummpt2co  33033  psgnfzto1stlem  33102  nsgmgc  33419  nsgqusf1olem1  33420  algextdeglem2  33723  algextdeglem4  33725  locfinreflem  33800  rspectopn  33827  zarcls  33834  zartopn  33835  prodindf  34003  gsumesum  34039  esumlub  34040  esumgect  34070  esum2d  34073  ldgenpisyslem1  34143  sxbrsigalem0  34252  omscl  34276  omsmon  34279  carsgclctunlem2  34300  carsgclctunlem3  34301  pmeasadd  34306  hgt750lemb  34649  mnurndlem2  44277  suprnmpt  45116  rnmptssrn  45124  wessf1ornlem  45127  rnmptssd  45138  rnmptssbi  45205  liminflelimsuplem  45730  fourierdlem53  46114  fourierdlem111  46172  ioorrnopnlem  46259  salexct3  46297  salgensscntex  46299  sge0rnre  46319  sge0tsms  46335  sge0cl  46336  sge0fsum  46342  sge0sup  46346  sge0gerp  46350  sge0pnffigt  46351  sge0lefi  46353  sge0xaddlem1  46388  sge0xaddlem2  46389  meadjiunlem  46420