Theorem rnmptss 7121

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

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

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 2733  ax-sep 5249  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-fun 6539  df-fn 6540  df-f 6541

This theorem is used by:  rnmptssd  7122  mptexw  7963  iunon  8340  iinon  8341  gruiun  10877  subdrgint  21053  smadiadetlem3lem2  22975  tgiun  23290  ustuqtop0  24552  metustss  24863  efabl  26871  efsubm  26872  fnpreimac  33257  prodindf  33422  swrdrn2  33510  gsummpt2co  33602  psgnfzto1stlem  33654  elrgspnsubrunlem1  33801  nsgmgc  33956  nsgqusf1olem1  33957  algextdeglem2  34343  algextdeglem4  34345  locfinreflem  34465  rspectopn  34492  zarcls  34499  zartopn  34500  gsumesum  34684  esumlub  34685  esumgect  34715  esum2d  34718  ldgenpisyslem1  34789  sxbrsigalem0  34896  omscl  34920  omsmon  34923  carsgclctunlem2  34944  carsgclctunlem3  34945  pmeasadd  34950  hgt750lemb  35278  mnurndlem2  45251  suprnmpt  46158  rnmptssrn  46166  wessf1ornlem  46169  rnmptssbi  46241  liminflelimsuplem  46754  fourierdlem53  47138  fourierdlem111  47196  ioorrnopnlem  47283  salexct3  47321  salgensscntex  47323  sge0rnre  47343  sge0tsms  47359  sge0cl  47360  sge0fsum  47366  sge0sup  47370  sge0gerp  47374  sge0pnffigt  47375  sge0lefi  47377  sge0xaddlem1  47412  sge0xaddlem2  47413  meadjiunlem  47444