Theorem rnmptss 7098

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∀wral 3045   ⊆ wss 3917   ↦ cmpt 5191  ran crn 5642  ⟶wf 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-fun 6516  df-fn 6517  df-f 6518

This theorem is referenced by:  mptexw  7934  iunon  8311  iinon  8312  gruiun  10759  subdrgint  20719  smadiadetlem3lem2  22561  tgiun  22873  ustuqtop0  24135  metustss  24446  efabl  26466  efsubm  26467  fnpreimac  32602  prodindf  32793  swrdrn2  32883  gsummpt2co  32995  psgnfzto1stlem  33064  elrgspnsubrunlem1  33205  nsgmgc  33390  nsgqusf1olem1  33391  algextdeglem2  33715  algextdeglem4  33717  locfinreflem  33837  rspectopn  33864  zarcls  33871  zartopn  33872  gsumesum  34056  esumlub  34057  esumgect  34087  esum2d  34090  ldgenpisyslem1  34160  sxbrsigalem0  34269  omscl  34293  omsmon  34296  carsgclctunlem2  34317  carsgclctunlem3  34318  pmeasadd  34323  hgt750lemb  34654  mnurndlem2  44278  suprnmpt  45175  rnmptssrn  45183  wessf1ornlem  45186  rnmptssd  45197  rnmptssbi  45261  liminflelimsuplem  45780  fourierdlem53  46164  fourierdlem111  46222  ioorrnopnlem  46309  salexct3  46347  salgensscntex  46349  sge0rnre  46369  sge0tsms  46385  sge0cl  46386  sge0fsum  46392  sge0sup  46396  sge0gerp  46400  sge0pnffigt  46401  sge0lefi  46403  sge0xaddlem1  46438  sge0xaddlem2  46439  meadjiunlem  46470