Theorem rnmptss 7107

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ∀wral 3061   ⊆ wss 3945   ↦ cmpt 5225  ran crn 5671  ⟶wf 6529

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5293  ax-nul 5300  ax-pr 5421

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5568  df-xp 5676  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-rn 5681  df-res 5682  df-ima 5683  df-fun 6535  df-fn 6536  df-f 6537

This theorem is referenced by:  mptexw  7923  iunon  8323  iinon  8324  gruiun  10778  subdrgint  20370  smadiadetlem3lem2  22100  tgiun  22413  ustuqtop0  23676  metustss  23991  efabl  25990  efsubm  25991  fnpreimac  31829  swrdrn2  32053  gsummpt2co  32135  psgnfzto1stlem  32194  nsgmgc  32443  nsgqusf1olem1  32444  locfinreflem  32715  rspectopn  32742  zarcls  32749  zartopn  32750  prodindf  32916  gsumesum  32952  esumlub  32953  esumgect  32983  esum2d  32986  ldgenpisyslem1  33056  sxbrsigalem0  33165  omscl  33189  omsmon  33192  carsgclctunlem2  33213  carsgclctunlem3  33214  pmeasadd  33219  hgt750lemb  33563  mnurndlem2  42876  suprnmpt  43705  rnmptssrn  43714  wessf1ornlem  43717  rnmptssd  43730  rnmptssbi  43802  liminflelimsuplem  44328  fourierdlem53  44712  fourierdlem111  44770  ioorrnopnlem  44857  salexct3  44895  salgensscntex  44897  sge0rnre  44917  sge0tsms  44933  sge0cl  44934  sge0fsum  44940  sge0sup  44944  sge0gerp  44948  sge0pnffigt  44949  sge0lefi  44951  sge0xaddlem1  44986  sge0xaddlem2  44987  meadjiunlem  45018