Theorem rnmptss 6990

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2109  ∀wral 3065   ⊆ wss 3891   ↦ cmpt 5161  ran crn 5589  ⟶wf 6426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-fun 6432  df-fn 6433  df-f 6434

This theorem is referenced by:  mptexw  7782  iunon  8154  iinon  8155  gruiun  10539  subdrgint  20052  smadiadetlem3lem2  21797  tgiun  22110  ustuqtop0  23373  metustss  23688  efabl  25687  efsubm  25688  fnpreimac  30987  swrdrn2  31205  gsummpt2co  31287  psgnfzto1stlem  31346  nsgmgc  31576  nsgqusf1olem1  31577  locfinreflem  31769  rspectopn  31796  zarcls  31803  zartopn  31804  prodindf  31970  gsumesum  32006  esumlub  32007  esumgect  32037  esum2d  32040  ldgenpisyslem1  32110  sxbrsigalem0  32217  omscl  32241  omsmon  32244  carsgclctunlem2  32265  carsgclctunlem3  32266  pmeasadd  32271  hgt750lemb  32615  mnurndlem2  41853  suprnmpt  42663  rnmptssrn  42672  wessf1ornlem  42675  rnmptssd  42688  rnmptssbi  42760  liminflelimsuplem  43270  fourierdlem53  43654  fourierdlem111  43712  ioorrnopnlem  43799  saliuncl  43817  salexct3  43835  salgensscntex  43837  sge0rnre  43856  sge0tsms  43872  sge0cl  43873  sge0fsum  43879  sge0sup  43883  sge0gerp  43887  sge0pnffigt  43888  sge0lefi  43890  sge0xaddlem1  43925  sge0xaddlem2  43926  meadjiunlem  43957