Theorem rnmptss 6863

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  ∀wral 3106   ⊆ wss 3881   ↦ cmpt 5110  ran crn 5520  ⟶wf 6320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-fv 6332

This theorem is referenced by:  mptexw  7636  iunon  7959  iinon  7960  gruiun  10210  subdrgint  19575  smadiadetlem3lem2  21272  tgiun  21584  ustuqtop0  22846  metustss  23158  efabl  25142  efsubm  25143  fnpreimac  30434  swrdrn2  30654  gsummpt2co  30733  psgnfzto1stlem  30792  locfinreflem  31193  rspectopn  31220  zarcls  31227  zartopn  31228  prodindf  31392  gsumesum  31428  esumlub  31429  esumgect  31459  esum2d  31462  ldgenpisyslem1  31532  sxbrsigalem0  31639  omscl  31663  omsmon  31666  carsgclctunlem2  31687  carsgclctunlem3  31688  pmeasadd  31693  hgt750lemb  32037  mnurndlem2  40990  suprnmpt  41798  rnmptssrn  41808  wessf1ornlem  41811  rnmptssd  41824  rnmptssbi  41899  liminflelimsuplem  42417  fourierdlem31  42780  fourierdlem53  42801  fourierdlem111  42859  ioorrnopnlem  42946  saliuncl  42964  salexct3  42982  salgensscntex  42984  sge0rnre  43003  sge0tsms  43019  sge0cl  43020  sge0fsum  43026  sge0sup  43030  sge0gerp  43034  sge0pnffigt  43035  sge0lefi  43037  sge0xaddlem1  43072  sge0xaddlem2  43073  meadjiunlem  43104  meadjiun  43105