Theorem rnmptss 7077

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∀wral 3052   ⊆ wss 3903   ↦ cmpt 5181  ran crn 5633  ⟶wf 6496

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-fun 6502  df-fn 6503  df-f 6504

This theorem is referenced by:  rnmptssd  7078  mptexw  7907  iunon  8281  iinon  8282  gruiun  10722  subdrgint  20748  smadiadetlem3lem2  22623  tgiun  22935  ustuqtop0  24196  metustss  24507  efabl  26527  efsubm  26528  fnpreimac  32760  prodindf  32955  swrdrn2  33047  gsummpt2co  33142  psgnfzto1stlem  33194  elrgspnsubrunlem1  33341  nsgmgc  33505  nsgqusf1olem1  33506  algextdeglem2  33896  algextdeglem4  33898  locfinreflem  34018  rspectopn  34045  zarcls  34052  zartopn  34053  gsumesum  34237  esumlub  34238  esumgect  34268  esum2d  34271  ldgenpisyslem1  34341  sxbrsigalem0  34449  omscl  34473  omsmon  34476  carsgclctunlem2  34497  carsgclctunlem3  34498  pmeasadd  34503  hgt750lemb  34834  mnurndlem2  44638  suprnmpt  45533  rnmptssrn  45541  wessf1ornlem  45544  rnmptssbi  45618  liminflelimsuplem  46133  fourierdlem53  46517  fourierdlem111  46575  ioorrnopnlem  46662  salexct3  46700  salgensscntex  46702  sge0rnre  46722  sge0tsms  46738  sge0cl  46739  sge0fsum  46745  sge0sup  46749  sge0gerp  46753  sge0pnffigt  46754  sge0lefi  46756  sge0xaddlem1  46791  sge0xaddlem2  46792  meadjiunlem  46823  sinnpoly  47251