Theorem rnmptssd 45190

Description: The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 11-Oct-2020.)

Hypotheses

Ref	Expression
rnmptssd.1	⊢ Ⅎ𝑥𝜑
rnmptssd.2	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
rnmptssd.3	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)

Assertion

Ref	Expression
rnmptssd	⊢ (𝜑 → ran 𝐹 ⊆ 𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶

Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem rnmptssd

Step	Hyp	Ref	Expression
1		rnmptssd.1	. . 3 ⊢ Ⅎ𝑥𝜑
2		rnmptssd.3	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)
3	1, 2	ralrimia 3236	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶)
4		rnmptssd.2	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
5	4	rnmptss 7095	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶)
6	3, 5	syl 17	1 ⊢ (𝜑 → ran 𝐹 ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  Ⅎwnf 1783   ∈ wcel 2109  ∀wral 3044   ⊆ wss 3914   ↦ cmpt 5188  ran crn 5639

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-fun 6513  df-fn 6514  df-f 6515

This theorem is referenced by:  infnsuprnmpt  45244  suprclrnmpt  45245  suprubrnmpt2  45246  suprubrnmpt  45247  fisupclrnmpt  45394  supxrleubrnmpt  45402  infxrlbrnmpt2  45406  supxrrernmpt  45417  suprleubrnmpt  45418  infrnmptle  45419  infxrunb3rnmpt  45424  supxrre3rnmpt  45425  supminfrnmpt  45441  infxrrnmptcl  45443  infxrgelbrnmpt  45450  infrpgernmpt  45461  supminfxrrnmpt  45467  liminfcl  45761  fourierdlem31  46136  fourierdlem53  46157  sge0xaddlem2  46432  sge0reuz  46445  sge0reuzb  46446  meadjiun  46464  hoidmvlelem2  46594  iunhoiioolem  46673  vonioolem1  46678  smflimsuplem4  46821