Theorem rnmptss 7122

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  ∀wral 3081   ⊆ wss 3906   ↦ cmpt 5194  ran crn 5664  ⟶wf 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-fun 6542  df-fn 6543  df-f 6544

This theorem is used by:  rnmptssd  7123  mptexw  7956  iunon  8332  iinon  8333  gruiun  10799  subdrgint  20956  smadiadetlem3lem2  22874  tgiun  23186  ustuqtop0  24448  metustss  24759  efabl  26766  efsubm  26767  fnpreimac  33086  prodindf  33252  swrdrn2  33340  gsummpt2co  33432  psgnfzto1stlem  33484  elrgspnsubrunlem1  33631  nsgmgc  33785  nsgqusf1olem1  33786  algextdeglem2  34172  algextdeglem4  34174  locfinreflem  34294  rspectopn  34321  zarcls  34328  zartopn  34329  gsumesum  34513  esumlub  34514  esumgect  34544  esum2d  34547  ldgenpisyslem1  34618  sxbrsigalem0  34726  omscl  34750  omsmon  34753  carsgclctunlem2  34774  carsgclctunlem3  34775  pmeasadd  34780  hgt750lemb  35108  mnurndlem2  45050  suprnmpt  45950  rnmptssrn  45958  wessf1ornlem  45961  rnmptssbi  46033  liminflelimsuplem  46547  fourierdlem53  46931  fourierdlem111  46989  ioorrnopnlem  47076  salexct3  47114  salgensscntex  47116  sge0rnre  47136  sge0tsms  47152  sge0cl  47153  sge0fsum  47159  sge0sup  47163  sge0gerp  47167  sge0pnffigt  47168  sge0lefi  47170  sge0xaddlem1  47205  sge0xaddlem2  47206  meadjiunlem  47237  sinnpoly  47686