Theorem rnmptss 7057

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∀wral 3044   ⊆ wss 3903   ↦ cmpt 5173  ran crn 5620  ⟶wf 6478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-fun 6484  df-fn 6485  df-f 6486

This theorem is referenced by:  mptexw  7888  iunon  8262  iinon  8263  gruiun  10693  subdrgint  20688  smadiadetlem3lem2  22552  tgiun  22864  ustuqtop0  24126  metustss  24437  efabl  26457  efsubm  26458  fnpreimac  32614  prodindf  32806  swrdrn2  32896  gsummpt2co  33001  psgnfzto1stlem  33042  elrgspnsubrunlem1  33187  nsgmgc  33349  nsgqusf1olem1  33350  algextdeglem2  33685  algextdeglem4  33687  locfinreflem  33807  rspectopn  33834  zarcls  33841  zartopn  33842  gsumesum  34026  esumlub  34027  esumgect  34057  esum2d  34060  ldgenpisyslem1  34130  sxbrsigalem0  34239  omscl  34263  omsmon  34266  carsgclctunlem2  34287  carsgclctunlem3  34288  pmeasadd  34293  hgt750lemb  34624  mnurndlem2  44255  suprnmpt  45152  rnmptssrn  45160  wessf1ornlem  45163  rnmptssd  45174  rnmptssbi  45238  liminflelimsuplem  45756  fourierdlem53  46140  fourierdlem111  46198  ioorrnopnlem  46285  salexct3  46323  salgensscntex  46325  sge0rnre  46345  sge0tsms  46361  sge0cl  46362  sge0fsum  46368  sge0sup  46372  sge0gerp  46376  sge0pnffigt  46377  sge0lefi  46379  sge0xaddlem1  46414  sge0xaddlem2  46415  meadjiunlem  46446  sinnpoly  46875