Theorem rnmptss 7116

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∀wral 3076   ⊆ wss 3899   ↦ cmpt 5186  ran crn 5656  ⟶wf 6529

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-pr 5398

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-fun 6535  df-fn 6536  df-f 6537

This theorem is used by:  rnmptssd  7117  mptexw  7950  iunon  8328  iinon  8329  gruiun  10808  subdrgint  20969  smadiadetlem3lem2  22889  tgiun  23204  ustuqtop0  24466  metustss  24777  efabl  26787  efsubm  26788  fnpreimac  33143  prodindf  33308  swrdrn2  33396  gsummpt2co  33488  psgnfzto1stlem  33540  elrgspnsubrunlem1  33687  nsgmgc  33841  nsgqusf1olem1  33842  algextdeglem2  34228  algextdeglem4  34230  locfinreflem  34350  rspectopn  34377  zarcls  34384  zartopn  34385  gsumesum  34569  esumlub  34570  esumgect  34600  esum2d  34603  ldgenpisyslem1  34674  sxbrsigalem0  34782  omscl  34806  omsmon  34809  carsgclctunlem2  34830  carsgclctunlem3  34831  pmeasadd  34836  hgt750lemb  35164  mnurndlem2  45106  suprnmpt  46006  rnmptssrn  46014  wessf1ornlem  46017  rnmptssbi  46089  liminflelimsuplem  46603  fourierdlem53  46987  fourierdlem111  47045  ioorrnopnlem  47132  salexct3  47170  salgensscntex  47172  sge0rnre  47192  sge0tsms  47208  sge0cl  47209  sge0fsum  47215  sge0sup  47219  sge0gerp  47223  sge0pnffigt  47224  sge0lefi  47226  sge0xaddlem1  47261  sge0xaddlem2  47262  meadjiunlem  47293