Theorem rnmptss 7066

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∀wral 3049   ⊆ wss 3899   ↦ cmpt 5177  ran crn 5623  ⟶wf 6486

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 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

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 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-fun 6492  df-fn 6493  df-f 6494

This theorem is referenced by:  mptexw  7895  iunon  8269  iinon  8270  gruiun  10708  subdrgint  20734  smadiadetlem3lem2  22609  tgiun  22921  ustuqtop0  24182  metustss  24493  efabl  26513  efsubm  26514  fnpreimac  32698  prodindf  32893  swrdrn2  32985  gsummpt2co  33080  psgnfzto1stlem  33131  elrgspnsubrunlem1  33278  nsgmgc  33442  nsgqusf1olem1  33443  algextdeglem2  33824  algextdeglem4  33826  locfinreflem  33946  rspectopn  33973  zarcls  33980  zartopn  33981  gsumesum  34165  esumlub  34166  esumgect  34196  esum2d  34199  ldgenpisyslem1  34269  sxbrsigalem0  34377  omscl  34401  omsmon  34404  carsgclctunlem2  34425  carsgclctunlem3  34426  pmeasadd  34431  hgt750lemb  34762  mnurndlem2  44465  suprnmpt  45360  rnmptssrn  45368  wessf1ornlem  45371  rnmptssd  45382  rnmptssbi  45446  liminflelimsuplem  45961  fourierdlem53  46345  fourierdlem111  46403  ioorrnopnlem  46490  salexct3  46528  salgensscntex  46530  sge0rnre  46550  sge0tsms  46566  sge0cl  46567  sge0fsum  46573  sge0sup  46577  sge0gerp  46581  sge0pnffigt  46582  sge0lefi  46584  sge0xaddlem1  46619  sge0xaddlem2  46620  meadjiunlem  46651  sinnpoly  47079