Theorem rnmptss 7155

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  ∀wral 3080   ⊆ wss 3900   ↦ cmpt 5192  ran crn 5659  ⟶wf 6562

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-fun 6568  df-fn 6569  df-f 6570

This theorem is used by:  rnmptssd  7156  mptexw  7999  iunon  8385  iinon  8386  gruiun  10923  subdrgint  21111  smadiadetlem3lem2  23037  tgiun  23352  ustuqtop0  24614  metustss  24925  efabl  26935  efsubm  26936  fnpreimac  33362  prodindf  33525  swrdrn2  33613  gsummpt2co  33708  psgnfzto1stlem  33760  elrgspnsubrunlem1  33907  nsgmgc  34067  nsgqusf1olem1  34068  algextdeglem2  34461  algextdeglem4  34463  locfinreflem  34583  rspectopn  34610  zarcls  34617  zartopn  34618  gsumesum  34802  esumlub  34803  esumgect  34833  esum2d  34836  ldgenpisyslem1  34907  sxbrsigalem0  35014  omscl  35038  omsmon  35041  carsgclctunlem2  35062  carsgclctunlem3  35063  pmeasadd  35068  hgt750lemb  35396  mnurndlem2  45527  suprnmpt  46462  rnmptssrn  46470  wessf1ornlem  46473  rnmptssbi  46545  liminflelimsuplem  47058  fourierdlem53  47442  fourierdlem111  47500  ioorrnopnlem  47587  salexct3  47625  salgensscntex  47627  sge0rnre  47647  sge0tsms  47663  sge0cl  47664  sge0fsum  47670  sge0sup  47674  sge0gerp  47678  sge0pnffigt  47679  sge0lefi  47681  sge0xaddlem1  47716  sge0xaddlem2  47717  meadjiunlem  47748